Theorem: LO.FirstOrder.Derivation.neg_ne_and (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q✝ r p q : SyntacticFormula L
⊢ complexity (~p) ≠ complexity (p ⋏ q)
Tactic:
simp
State after:
no goals