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