proposition: Theorem Permuted_merge_list_to_stack : forall stack l, Permutation (l ++ flatten_stack stack) (flatten_stack (merge_list_to_stack stack l)).
proof: Proof. induction stack as [|[]]; simpl; intros. - reflexivity. - rewrite app_assoc. etransitivity. + apply Permutation_app_tail. etransitivity. * apply Permutation_app_comm. * apply Permuted_merge. + apply IHstack. - reflexivity. Qed.
imports: List Setoid Permutation Sorted Orders