proposition: Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m).
proof: Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f (this m) x e). Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia