proposition: Lemma cnf_of_literal_correct : forall (m: hmap) g cp cm ar l (WF:has_form m (form_of_literal l)), (Forall eval_watched_clause (snd (cnf_of_literal l (is_classic g) cp cm ar nil (elt (form_of_literal l)) (form_of_literal l))) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. unfold cnf_of_literal. intros. apply cnf_correct_opt with (m:=m) in H ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause