{k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          {motive : FiniteGaloisIntermediateField k K → Sort u} →
            ((toIntermediateField : IntermediateField k K) →
                [finiteDimensional : FiniteDimensional k ↥toIntermediateField] →
                  [isGalois : IsGalois k ↥toIntermediateField] →
                    motive
                      { toIntermediateField := toIntermediateField, finiteDimensional := finiteDimensional,
                        isGalois := isGalois }) →
              (t : FiniteGaloisIntermediateField k K) → motive t