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