proposition: Lemma cnf_minus_impl_correct : forall l r hf g acc (EQ : elt hf = LIMPL l r) (ACC : (Forall eval_watched_clause acc -> eval_ohformula g) -> eval_ohformula g), (Forall eval_watched_clause (cnf_minus_impl l r hf acc) -> eval_ohformula g) -> eval_ohformula g.
proof: Proof. unfold cnf_plus_impl. intros. apply ACC. intro ACC'; clear ACC. apply H; clear H. unfold cnf_minus_impl. destruct (watch_clause_of_list (NEG hf :: xrev_map NEG (unit_or r) l)) eqn:WC;auto. constructor ; auto. apply eval_watched_clause_of_list in WC ; auto. rewrite xmap_rev. change (NEG hf :: List.map NEG (rev l) ++ (unit_or r)) with (List.map NEG (hf ::rev l) ++ (unit_or r)). rewrite eval_literal_list_NEG_app. simpl. unfold eval_hformula at 1. rewrite EQ. simpl. intros. rewrite eval_and_list_rev in H. rewrite <- eval_impl_list_eq in H. rewrite eval_and_list_eq in H. unfold eval_hformula. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause