∀ (R : Type u_2) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Algebra.FormallyUnramified R S] [inst_4 : Algebra.EssFiniteType R S] (I : Type u_1) (b : Module.Basis I R S)
  (motive : (∃ a, Algebra.FormallyUnramified.elem R S = a.sum fun i x => x ⊗ₜ[R] b i) → Prop)
  (x : ∃ a, Algebra.FormallyUnramified.elem R S = a.sum fun i x => x ⊗ₜ[R] b i),
  (∀ (f : I →₀ S) (hf : Algebra.FormallyUnramified.elem R S = f.sum fun i x => x ⊗ₜ[R] b i), motive ⋯) → motive x