proposition: Lemma wf_cnf_minus_impl : forall m l r hf acc (HF1: Forall (has_form m) l) (HFr : has_form m r) (HF: has_form m hf) (HACC: Forall (has_watched_clause m) acc), Forall (has_watched_clause m) (cnf_minus_impl l r hf acc).
proof: Proof. unfold cnf_minus_impl. intros. destruct_in_goal WC; auto. constructor ; auto. eapply wf_watch_clause_of_list in WC; eauto. rewrite xmap_rev. constructor ; auto. rewrite Forall_app;split ; auto. rewrite map_rev. rewrite Forall_rev_iff. rewrite Forall_forall. rewrite Forall_forall in HF1. intros. rewrite in_map_iff in H. destruct H. destruct H ; subst. apply HF1;auto. apply wf_unit_or; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause