proposition: Lemma KVEnsemble_EquivalentKeys_Refl {B} : forall (ens : Ensemble (Key * B)), KVEnsemble_EquivalentKeys ens ens.
proof: Proof. unfold KVEnsemble_EquivalentKeys, EnsembleRemoveKey in *; simpl in *; intuition; 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