proposition: Lemma fold_lemma : forall {A: Type} (UP: A -> int -> (Annot.t watched_clause) -> A) (P: A -> Annot.t watched_clause -> Prop) Q m acc (WFm : WMap.wf_watch_map m) (Pacc : WMap.Forall_watch_map (P acc) m) (PUP : forall acc i e e', P acc e -> P acc e' -> Q acc -> P (UP acc i e) e') (UPOK : forall acc a, Q acc -> WMap.Forall_watch_map (P acc) m -> P acc (snd a) -> Q (UP acc (fst a) (snd a))) (Qacc : Q acc) , Q (WMap.fold_watch_map UP m acc).
proof: Proof. intros. rewrite WMap.fold_elements. assert (ALL : forall x, In x (WMap.elements m nil) -> P acc (snd x)). { intros. eapply WMap.in_elements; eauto. } revert acc Qacc Pacc ALL. induction ((WMap.elements m nil)). - simpl. auto. - simpl; intros. assert (ALLA := ALL _ (or_introl eq_refl)). apply IHl; auto. revert Pacc. apply WMap.Forall_watch_map_Forall. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause