Theorem: LO.FirstOrder.Semiformula.ex_ne_subst (Logic/FirstOrder/Basic/Syntax/Rew.lean)

State before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ 1
t : Semiterm L ξ 0
⊢ ([→ t].hom p).complexity ≠ (∃' p).complexity
Tactic:
simp
State after:
no goals