proposition: Lemma hconsmap_fold_update : forall {A: Type} (F: A -> state -> dresult), (forall x st, hconsmap_progress (F x) st) -> forall l st, hconsmap_progress (fold_update F l) st.
proof: Proof. unfold hconsmap_progress. induction l; simpl; auto. intros. specialize (H a st). destruct (F a st) eqn:EQ; simpl in *; try tauto. rewrite <- H ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause