proposition: Lemma mapoL_sorted l acc : sort O.ltk (rev l) -> sort O.ltk acc -> l < acc -> sort O.ltk (mapoL f l acc).
proof: Proof. revert acc. induction l as [|(k,e) l IH]; simpl; auto. intros acc Sl Sacc AP. rewrite sort_app_key in Sl; ok. destruct Sl as (Sl & _ & AP'). apply -> ApartL_rev in AP'. apply -> ApartL_consl in AP. destruct AP as (AP1,AP). apply IH; clear IH; simpl; auto; destruct (f k e); simpl; auto. - apply sort_cons_key. eauto using ApartL_eqk_l with map. - apply ApartL_consr. eauto using ApartL_eqk_r with map. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)