proposition: Lemma in_elements : forall P m (WF : wf_watch_map m) (PAll: Forall_watch_map P m) x (IN : In x (elements m nil)), P (snd x).
proof: Proof. intros. unfold IntMapForall in PAll. apply PAll with (k:=fst x). destruct x. apply IntMap.in_elements' with (opt:= None) in IN; auto. simpl in *. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause