proposition: Lemma FMapCommonKeys_find_None {A B} : forall m m' k, FMapCommonKeys m m' -> StringIndexedMap.find (elt:=A) k m = None -> StringIndexedMap.find (elt:=B) k m' = None .
proof: Proof. intros. caseEq (StringIndexedMap.find (elt:=B) k m'); eauto. apply StringIndexedMap.find_2 in H1. apply H in H1. destruct_ex. apply StringIndexedMap.find_1 in H1. rewrite H1 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