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