∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {s : L.Substructure M}
  (motive : (∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = s) → Prop)
  (x : ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = s),
  (∀ (t : Set M) (ht : t.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun t = s), motive ⋯) → motive x