proposition: Lemma eval_annot_add_clause : forall m l i wc cls (WF: WMap.wf cls) (EC: eval_annot_clauses m cls) (EW: eval_annot eval_watched_clause m wc), eval_annot_clauses m (WMap.add_clause l i wc cls).
proof: Proof. unfold eval_annot_clauses. intros. apply WMap.Forall_add_clause; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause