∀ {F : Type u_2} {E : Type u_1} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K L : IntermediateField F E)
  [inst_3 : Normal F ↥K]
  (motive :
    (x : ↥K) →
      x ∈ IntermediateField.fixedField (IntermediateField.restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range → Prop)
  (x : ↥K)
  (hx₂ : x ∈ IntermediateField.fixedField (IntermediateField.restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range),
  (∀ (x : E) (hx₁ : x ∈ K)
      (hx₂ :
        ⟨x, hx₁⟩ ∈ IntermediateField.fixedField (IntermediateField.restrictRestrictAlgEquivMapHom F (↥K) (↥L) E).range),
      motive ⟨x, hx₁⟩ hx₂) →
    motive x hx₂