proposition: Lemma wf_cnf_of_op_plus : forall m b o l hf acc (HF1: Forall (has_form m) l) (HF: has_form m hf) (HACC: Forall (has_watched_clause m) acc), Forall (has_watched_clause m) (cnf_of_op_plus b o l hf acc).
proof: Proof. unfold cnf_of_op_plus. intros. destruct o ; auto. - unfold cnf_plus_and. destruct_in_goal WC;[constructor|];auto. eapply wf_watch_clause_of_list in WC; eauto. rewrite xmap_rev. rewrite Forall_app. rewrite map_rev. rewrite Forall_rev_iff. split. apply Forall_has_literal_NEG; auto. constructor ; auto. - unfold cnf_plus_or. rewrite xmap_rev. rewrite Forall_app. rewrite map_rev. rewrite Forall_rev_iff. split; auto. rewrite Forall_forall. intros. rewrite in_map_iff in H. destruct H. destruct H. subst. unfold has_watched_clause. simpl. rewrite Forall_rew;auto. split;auto. rewrite Forall_forall in HF1. apply HF1; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause