proposition: Lemma refine_pick_repInvAbsR : forall r_o, repInv r_o -> refineEquiv {r_n | repInvAbsR r_o r_n} (ret r_o).
proof: Proof. unfold repInvAbsR; split; intros v CompV; computes_to_inv; intuition; subst; computes_to_econstructor; eauto. Qed.
imports: Fiat.Common Fiat.Computation Coq.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements