proposition: Lemma mergeL_sorted f l l' acc : sort O.ltk (rev l) -> sort O.ltk (rev l') -> sort O.ltk acc -> l < acc -> l' < acc -> sort O.ltk (mergeL f l l' acc).
proof: Proof. revert l' acc. induction l as [|(x,e) l IHl]. - simpl. intros. apply mapoL_sorted; auto. - induction l' as [|(x',e') l' IHl']. + intros. apply mapoL_sorted; auto. + intros acc Sl Sl' Sacc AP AP'. simpl in Sl, Sl'. assert (Sl0 := Sl). assert (Sl0' := Sl'). assert (AP0 := AP). assert (AP0' := AP'). apply sort_app_key in Sl. destruct Sl as (Sl & _ & APl). apply sort_app_key in Sl'. destruct Sl' as (Sl' & _ & APl'). apply -> ApartL_rev in APl. apply -> ApartL_rev in APl'. apply -> ApartL_consl in AP. destruct AP as (AP1,AP). apply -> ApartL_consl in AP'. destruct AP' as (AP1',AP'). rewrite mergeL_eqn; destmatch; [intro EQ|intro LT|intro LT]; apply IHl || apply IHl'; clear IHl IHl'; auto; destruct f; simpl; auto; try apply sort_cons_key; try apply ApartL_consr; try apply ApartL_consl; split; auto; eauto using ApartL_eqk_l, ApartL_eqk_r with map; apply ApartL_consl; split; try (eapply ApartL_ltk_r; eautom; fail); intros (?,?) (?,?); compute; intuition congruence. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)