proposition: Lemma refine_pick_cachedRep : forall or, refine {nr | cachedRep_AbsR or nr} (cv <- {cv | cacheSpec or cv}; ret {| origRep := or; cachedVal := cv |}).
proof: Proof. unfold refine; intros or v ComputesTo_v; computes_to_inv; subst; econstructor; unfold cachedRep_AbsR; simpl; intuition. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv