proposition: Lemma wf_cnf_of_op_minus : 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_minus b o l hf acc).
proof: Proof. unfold cnf_of_op_plus. intros. destruct o ; auto. - simpl. unfold cnf_minus_and. 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. repeat rewrite Forall_rew;auto. repeat split ; auto. rewrite Forall_forall in HF1. apply HF1;auto. - simpl. unfold cnf_minus_or. destruct l; simpl; auto. rewrite Forall_rew. split ; auto. unfold has_watched_clause. simpl. inv HF1. rewrite Forall_rew;split; auto. rewrite Forall_rew;split; auto. unfold rev_map. rewrite xmap_rev. rewrite app_nil_r. rewrite map_rev. rewrite Forall_rev_iff. apply Forall_has_literal_POS;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause