proposition: Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
proof: Proof. intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl. apply map_2; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia