proposition: Lemma FMapCommonKeys_remove {A B} : forall k (ens : StringIndexedMap.t A) (ens' : StringIndexedMap.t B), FMapCommonKeys ens ens' -> FMapCommonKeys (StringIndexedMap.remove k ens) (StringIndexedMap.remove k ens').
proof: Proof. unfold FMapCommonKeys; intuition; (destruct (string_dec k0 k); [subst; exfalso; eapply (StringIndexedMap.remove_1); eauto; unfold StringIndexedMap.In, StringIndexedMap.Raw.In0, StringIndexedMap.MapsTo in *; simpl in *; eauto | eapply StringIndexedMap.remove_3 in H0; apply H in H0; destruct_ex; eauto using StringIndexedMap.remove_2 ]). 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