proposition: Theorem Permuted_merge_stack : forall stack, Permutation (flatten_stack stack) (merge_stack stack).
proof: Proof. induction stack as [|[]]; simpl. - trivial. - transitivity (l ++ merge_stack stack). + apply Permutation_app_head; trivial. + apply Permuted_merge. - assumption. Qed.
imports: List Setoid Permutation Sorted Orders