proposition: Lemma KVEnsemble_EquivalentKeys_Update {B C} : forall (ens : Ensemble (Key * B)) (ens' : Ensemble (Key * C)) (EquivKeys : KVEnsemble_EquivalentKeys ens ens') k f g, KVEnsemble_EquivalentKeys (EnsembleUpdateKey k ens f) (EnsembleUpdateKey k ens' g).
proof: Proof. unfold KVEnsemble_EquivalentKeys, EnsembleUpdateKey, EnsembleReplaceKey, EnsembleRemoveKey in *; simpl in *; intuition; injections; eauto; subst. destruct_ex; intuition; eauto; subst. apply H in H3; destruct_ex; eauto. exists (g x0); left; intuition; eauto. apply H in H3; destruct_ex; eauto. destruct_ex; intuition; subst. apply H0 in H3; destruct_ex; eexists; left; intuition; eauto. apply H0 in H3; 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