proposition: Theorem sort_aux1_permutation : forall l:list (list A), permutation (app_all (sort_aux1 l)) (app_all l).
proof: Proof. intros l; elim l using list_ind2. - simpl in |- *; constructor. - simpl in |- *; intros; apply permutation_reflexive. - intros l1 l2 tl Hrec; simpl in |- *. rewrite app_assoc. apply permutation_app4;auto. apply merge_permutation; auto. Qed.
imports: List Lia