∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (motive : ⊤.FG → Prop)
  (x : ⊤.FG), (∀ (s : Finset E) (hs : IntermediateField.adjoin F ↑s = ⊤), motive ⋯) → motive x