proposition: Lemma wf_find_clauses : forall m i cls (WF : WMap.wf cls) (WFCL : has_clauses m cls), (WMap.Forall_watch_map (check_annot has_watched_clause m) (WMap.find_clauses i cls)) /\ WMap.wf_watch_map (WMap.find_clauses i cls).
proof: Proof. intros. split. - apply WMap.find_clauses_Forall. auto. - apply WMap.wf_find_clauses;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause