proposition: Lemma refine_pick_repInvAbsR' : forall r_n, repInv r_n -> refineEquiv {r_o | repInvAbsR r_o r_n} (ret r_n).
proof: Proof. unfold repInvAbsR; split; intros v CompV; computes_to_inv; intuition; subst; 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