proposition: Lemma cnf_correct_opt : forall m (f : LForm) (pol : bool) (g : option HFormula) (cp cm : IntMap.ptrie unit) (ar : list literal) (acc : list watched_clause) (hf : t LForm), has_form m hf -> elt hf = f -> ((Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g) -> (Forall eval_watched_clause (snd (cnf pol (is_classic g) cp cm ar acc f hf)) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. destruct pol. - apply cnf_correct. - intros *. apply cnf_correct. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause