proposition: Lemma refine_pick_KVEnsembleUpdateKey {B C} : forall (ens : Ensemble (Key * B)) (ens' : Ensemble (Key * C)) (EquivKeys : KVEnsemble_EquivalentKeys ens ens') k f, refine {ens'' | KVEnsemble_EquivalentKeys (EnsembleUpdateKey k ens f) ens''} (b <- {b | @PickID C b}; ret (EnsembleUpdateKey k ens' (fun _ => b))).
proof: Proof. unfold refine; intros; inversion_by computes_to_inv; subst; econstructor. eauto using KVEnsemble_EquivalentKeys_Update. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec