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

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