∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.Substructure M)
  (htv :
    ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M),
      φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)),
  ↑(S.toElementarySubstructure htv) = S