Theorem: LeanSAT.Model.PropFun.eq_bot_iff (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
φ : PropFun ν
h : φ = ⊥
⊢ ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
Tactic:
simp [h]
State after:
no goals

State before:
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
⊢ φ = ⊥
Tactic:
ext
State after:
case a
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
τ✝ : PropAssignment ν
⊢ τ✝ ⊨ φ ↔ τ✝ ⊨ ⊥

State before:
case a
ν : Type u_1
φ : PropFun ν
h : ∀ (τ : PropAssignment ν), (fun M φ => ¬M ⊨ φ) τ φ
τ✝ : PropAssignment ν
⊢ τ✝ ⊨ φ ↔ τ✝ ⊨ ⊥
Tactic:
simp [h]
State after:
no goals