Theorem: LO.FirstOrder.Semiformula.eval_existsUnique (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝¹ : Operator.Eq L
M : Type u_2
s : Structure L M
inst✝ : Structure.Eq L M
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L μ (n + 1)
⊢ (Eval s e ε) (∃'! p) ↔ ∃! x, (Eval s (x :> e) ε) p
Tactic:
simp [existsUnique, Semiformula.eval_substs, Matrix.comp_vecCons', ExistsUnique]
State after:
no goals