∀ (F : Type u_2) [inst : Field F] {E : Type u_1} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
  (motive : ↥(IntermediateField.adjoin F S) → Prop) (x : ↥(IntermediateField.adjoin F S)),
  (∀ (val : E) (h : val ∈ IntermediateField.adjoin F S), motive ⟨val, h⟩) → motive x