proposition: Lemma refine_pick_KVEnsembleInsertRemove {B C} : forall (ens : Ensemble (Key * B)) (ens' : Ensemble (Key * C)) (EquivKeys : KVEnsemble_EquivalentKeys ens ens') (ab : Key * B) k, refine {ens'' | KVEnsemble_EquivalentKeys (EnsembleInsert ab (EnsembleRemoveKey k ens)) ens''} (b <- {b | @PickID C b}; ret (EnsembleInsert (fst ab, b) (EnsembleRemoveKey k ens'))).
proof: Proof. unfold refine; intros; inversion_by computes_to_inv; subst; econstructor. eauto using KVEnsemble_EquivalentKeys_Insert, KVEnsemble_EquivalentKeys_Remove. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec