no goals
L : Language
L' : Language
M : Type w
N : Type ?u.259032
P : Type ?u.259035
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
φ : Formula L α
⊢ M ⊨ ↑equivSentence φ ↔ Realize φ fun a => ↑(Language.con L a)
rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]