proposition: Lemma Forall_watch_map_ForallAnd : forall (P Q: Annot.t watched_clause -> Prop) m, Forall_watch_map P m -> Forall_watch_map Q m -> Forall_watch_map (fun cl => P cl /\ Q cl) m.
proof: Proof. intros. apply IntMapForallAnd; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause