proposition: Lemma FMapCommonKeys_add {A B} : forall k a b (ens : StringIndexedMap.t A) (ens' : StringIndexedMap.t B), FMapCommonKeys ens ens' -> FMapCommonKeys (StringIndexedMap.add k a ens) (StringIndexedMap.add k b ens').
proof: Proof. unfold FMapCommonKeys; intuition; (destruct (string_dec k0 k); [eexists; eapply StringIndexedMap.add_1; eauto | eapply StringIndexedMap.add_3 in H0; eauto; apply H in H0; destruct_ex; eexists; eapply StringIndexedMap.add_2; eauto]). 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