simp[isVType] at h
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q : Semiformula L μ (n + 1)
h : (∀' q).isVType = true
⊢ False
no goals