proposition: Lemma hconsmap_map_dresult : forall F, (forall st, hconsmap_progress F st) -> (forall st, hconsmap_progress_r (map_dresult F) st).
proof: Proof. unfold hconsmap_progress_r. intros. destruct st ; simpl in *; auto. apply H ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause