Theorem: dpllSatYesSpec (LAMR/Examples/using_sat_solvers/dpll.lean)

State before:
⊢ ∀ (ϕ : CnfForm) (τ : PropAssignment), dpllSat ϕ = some τ ↔ PropAssignment.evalCnf τ ϕ = true
Tactic:
admit
State after:
no goals