proposition: Theorem Permuted_merge : forall l1 l2, Permutation (l1++l2) (merge l1 l2).
proof: Proof. induction l1; simpl merge; intro. - assert (forall l, (fix merge_aux (l0 : list t) : list t := l0) l = l) as -> by (destruct l; trivial). apply Permutation_refl. - induction l2. + rewrite app_nil_r. apply Permutation_refl. + destruct (a <=? a0). * constructor; apply IHl1. * apply Permutation_sym, Permutation_cons_app, Permutation_sym, IHl2. Qed.
imports: List Setoid Permutation Sorted Orders