Theorem: LO.FirstOrder.Interpretation.translationAux_neg (Logic/FirstOrder/Interpretation.lean)

State before:
L L' : Language
inst✝ : L.Eq
T : Theory L
ι : Interpretation T L'
n : ℕ
p : Semisentence L' n
⊢ ι.translationAux (~p) = ~ι.translationAux p
Tactic:
induction p using Semiformula.rec' <;> simp [translationAux, *, ←Semiformula.neg_eq]
State after:
no goals