proposition: Lemma KVEnsemble_EquivalentKeys_Insert {B C} : forall (ens : Ensemble (Key * B)) (ens' : Ensemble (Key * C)) (EquivKeys : KVEnsemble_EquivalentKeys ens ens') (ab : Key * B) (c : C), KVEnsemble_EquivalentKeys (EnsembleInsert ab ens) (EnsembleInsert (fst ab, c) ens').
proof: Proof. unfold refine; intros. unfold KVEnsemble_EquivalentKeys, EnsembleInsert in *; simpl in *; intuition; injections; eauto. apply H in H2; destruct_ex; eauto. apply H0 in H2; 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