Theorem: LeanSAT.Encode.Tseitin.NegNormForm.const_toPropFun (LeanSAT/Encode/Tseitin.lean)

State before:
ν : Type u_1
b : Bool
⊢ toPropFun (const b) = if b = true then ⊤ else ⊥
Tactic:
ext τ
State after:
case a
ν : Type u_1
b : Bool
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (const b) ↔ τ ⊨ if b = true then ⊤ else ⊥

State before:
case a
ν : Type u_1
b : Bool
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (const b) ↔ τ ⊨ if b = true then ⊤ else ⊥
Tactic:
cases b <;> simp [const, toPropFun]
State after:
no goals