proposition: Lemma mapi_1_eq (elt elt':Type)(m: t elt)(x:key)(e:elt) (f:key->elt->elt') : MapsTo x e m -> MapsTo x (f x e) (mapi f m).
proof: Proof. intro H; eapply mapi_1 in H; unfold E.eq in *. destruct H as [? [? ?]]; subst; eassumption. Qed.
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.FSets.FMapInterface Coq.FSets.FMapPositive Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.Prod