proposition: Lemma cnf_of_op_plus_correct : forall acc g o l hf (EQ : hf.(elt) = LOP o l) (ACC : (Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g), (Forall eval_watched_clause (cnf_of_op_plus (is_classic g) o l hf acc) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. destruct o ; simpl. - intros. apply ACC. intro. apply H. unfold cnf_plus_and. destruct (watch_clause_of_list (xrev_map NEG (POS hf:: nil) l)) eqn:WC;auto. constructor;auto. apply eval_watched_clause_of_list in WC ; auto. apply eval_literal_list_plus_and; auto. - intros. apply ACC. intro. apply H. unfold cnf_plus_or. rewrite xmap_rev. apply Forall_app. split ; auto. rewrite map_rev. apply Forall_rev. apply eval_plus_or; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause