proposition: Lemma Forall_watch_map_Forall : forall (P Q: Annot.t watched_clause -> Prop) m, (forall x, P x -> Q x) -> Forall_watch_map P m -> Forall_watch_map Q m.
proof: Proof. intros. eapply IntMapForall_Forall; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause