induction p using rec' <;> simp[Rew.rel, Rew.nrel, isVType]
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
no goals