proposition: Lemma hconsmap_comp : forall (F: state -> dresult) (G : state -> state), (hconsmap_eq G) -> (forall st, hconsmap_progress F st) -> (forall st, hconsmap_progress (fun st => F (G st)) st).
proof: Proof. unfold hconsmap_progress. intros. rewrite <- H. apply H0; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause