proposition: Lemma map_lelistA : forall (m: t elt)(x:key)(e:elt)(e':elt')(f:elt->elt'), lelistA (@ltk elt) (x,e) m -> lelistA (@ltk elt') (x,e') (map f m).
proof: Proof. induction m; simpl; auto. intros. destruct a as (x0,e0). inversion_clear H; auto. Qed.
imports: FMapInterface