proposition: Lemma eval_annot_add_watched_clause : forall i wc st (WF : wf_state st) (ES : eval_annot_state st) (EC : eval_annot eval_watched_clause (hconsmap st) wc), eval_annot_state (add_watched_clause st i wc).
proof: Proof. unfold add_watched_clause. intros. destruct ES ; destruct WF ; constructor ; auto. simpl. apply eval_annot_add_clause;auto with wf. apply WMap.wf_add_clause;auto. apply eval_annot_add_clause;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause