proposition: Lemma refine_pick_KeyToBeReplaced_never : forall (r : Ensemble (Key * Value)), refine {k_opt | forall k', k_opt = Some k' -> exists v', r (k', v')} (ret None).
proof: Proof. intros; rewrite refine_pick_val; [ reflexivity | discriminate ]. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec