Theorem: LO.FirstOrder.Semiformula.isVType_neg_true_of_eq_false (Logic/FirstOrder/Hauptsatz.lean)

State before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
n : ℕ
p : SyntacticSemiformula L n
⊢ isVType p = false → (~p).isVType = true
Tactic:
induction p using rec' <;> simp[Rew.rel, Rew.nrel, isVType]
State after:
no goals