proposition: Lemma fold_elements : forall (B : Type) (f : B -> int -> Annot.t watched_clause -> B) (m : watch_map) (v : B), fold_watch_map f m v = fold_left (fun (a : B) (p : int * Annot.t watched_clause) => f a (fst p) (snd p)) (elements m nil) v.
proof: Proof. intros. apply IntMap.fold_elements'. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause