proposition: Lemma wf_add_watched_clause : forall i wc st (WFC: check_annot has_watched_clause (hconsmap st) wc) (WFS: wf_state st), wf_state (add_watched_clause st i wc).
proof: Proof. intros. destruct WFS ; constructor ; auto with wf. - simpl. repeat apply wf_map_add_wneg_lit; auto. - simpl. inv WFC. inv wf_elt0. inv H2. repeat apply wf_add_wneg_lit ; auto. apply wf_map_add_wneg_lit; auto. - simpl. apply wf_add_clause; auto with wf. apply WMap.wf_add_clause;auto. apply wf_add_clause; auto with wf. - simpl. apply WMap.wf_add_clause ;auto with wf. apply WMap.wf_add_clause ;auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause