proposition: Lemma eval_annot_find_clauses : forall m i wc, WMap.Forall (eval_annot eval_watched_clause m) wc -> WMap.Forall_watch_map (eval_annot eval_watched_clause m) (WMap.find_clauses i wc).
proof: Proof. intros. apply WMap.find_clauses_Forall; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause