Theorem: LO.FirstOrder.Semiformula.ne_and_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 q r : Semiformula L μ n
h : p.isVType = true
⊢ p ≠ q ⋏ r
Tactic:
rintro rfl
State after:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q r : Semiformula L μ n
h : (q ⋏ r).isVType = true
⊢ False

State before:
L : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n : ℕ
q r : Semiformula L μ n
h : (q ⋏ r).isVType = true
⊢ False
Tactic:
simp[isVType] at h
State after:
no goals