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

State before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
p : Semiformula L μ n
q : Semiformula L μ (n + 1)
h : p.isVType = true
⊢ p ≠ ∀' q
Tactic:
rintro rfl
State after:
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

State before:
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
Tactic:
simp[isVType] at h
State after:
no goals