Theorem: LeanSAT.Model.PropForm.eval_ofBool (LeanSAT/Model/OfFun.lean)

State before:
ν✝ : Type u_1
τ : PropAssignment ν✝
b : Bool
⊢ eval τ (ofBool b) = b
Tactic:
cases b <;> simp
State after:
no goals