proposition: Lemma refine_LogIndexUsedKey : forall n or nr, CacheADTwLogIndex_AbsR or nr -> refine {b | decides b (usedKey or n)} {b | decides b (usedKey (fst nr) n)}.
proof: Proof. unfold CacheADTwLogIndex_AbsR, KVEnsemble_EquivalentKeys; intros; apply refine_pick_pick; unfold usedKey; simpl; intros; unfold decides; find_if_inside; simpl in * ; destruct_ex; unfold Same_set, Included, In in *; intuition; subst; 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