proposition: Lemma refine_pick_KeyToBeReplaced_min : forall (r : Ensemble (Key * Value) * Ensemble (Key * nat)), refine {k_opt | forall k', k_opt = Some k' -> exists v', fst r (k', v')} {k_opt | forall k', k_opt = Some k' -> ((exists v', fst r (k', v')) /\ (forall idx ki, snd r (k', idx) -> snd r ki -> idx <= snd ki)) }.
proof: Proof. intros; apply refine_pick_pick; intros. eapply H; 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