Theorem: LO.FirstOrder.Semiformula.isVType_shift_iff (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
⊢ ((Rew.hom ⇑) p).isVType = isVType p
Tactic:
induction p using rec' <;> simp[Rew.rel, Rew.nrel, isVType]
State after:
no goals