proposition: Lemma eval_find_clauses : forall i m, WMap.Forall (Annot.lift eval_watched_clause) m -> WMap.Forall_watch_map (Annot.lift eval_watched_clause) (WMap.find_clauses i m).
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