proposition: Lemma decides_usedKey : forall (or : Ensemble (string * Value)) (nr : StringIndexedMap.t Value) (k : string), EnsembleFMapEquivalence or nr -> decides (if StringIndexedMap.find k nr then true else false) (usedKey or k).
proof: Proof. unfold EnsembleFMapEquivalence, usedKey; intros; pose proof (H k); intuition. find_if_inside; simpl; eauto. intuition; destruct_ex. apply H2 in H0; discriminate. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements String_as_OT FMapAVL