Theorem: LO.FirstOrder.Semiformula.subfEquiv_neg_eq_neg_subfEquiv (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
p : Semiformula L μ n
⊢ ↑(subfEquiv (~p)) = (↑(subfEquiv p)).neg
Tactic:
induction p using rec' <;> simp[UFormula.neg, UTerm.ofSubterm_eq_subtEquiv, UFormula.ofSubformula_eq_subfEquiv, *]
State after:
no goals