proposition: Lemma wf_cnf_plus_impl : forall m b 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_plus_impl b l r hf acc).
proof: Proof. unfold cnf_plus_impl. intros. rewrite Forall_rew. split. - repeat constructor ; auto. - rewrite xmap_filter_rev. rewrite Forall_app. split; auto. rewrite map_rev. rewrite Forall_rev_iff. rewrite Forall_forall. intros. rewrite in_map_iff in H. destruct H. destruct H ; subst. rewrite filter_In in H0. destruct H0 as (H0 & _). unfold has_watched_clause. simpl. repeat rewrite Forall_rew; auto. repeat 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