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

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

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

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