∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {α : Type u'} [inst_1 : (L.withConstants α).Structure M]
  [(L.lhomWithConstants α).IsExpansionOn M] (φ : L.Formula α),
  M ⊨ FirstOrder.Language.Formula.equivSentence φ = φ.Realize fun a => ↑(L.con a)