proposition: Lemma refine_LogIndexEmpty : refine {nr' | CacheADTwLogIndex_AbsR (fun _ : Key * Value => False) nr'} (ret (fun _ => False, fun _ => False)).
proof: Proof. apply refine_pick_val; unfold CacheADTwLogIndex_AbsR, KVEnsemble_EquivalentKeys; intuition; destruct_ex; 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