proposition: Lemma refine_pick_CacheADTwLogIndex_AbsR or' : refine {nr' | CacheADTwLogIndex_AbsR or' nr'} (nr' <- {nr' | KVEnsemble_EquivalentKeys or' nr'}; ret (or', nr')).
proof: Proof. unfold CacheADTwLogIndex_AbsR; intros. setoid_rewrite refineEquiv_pick_pair_snd_dep; simpl. refine pick val or'. simplify with monad laws; f_equiv. unfold Same_set, Included; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec