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