proposition: Theorem Permuted_iter_merge : forall l stack, Permutation (flatten_stack stack ++ l) (iter_merge stack l).
proof: Proof. induction l; simpl; intros. - rewrite app_nil_r. apply Permuted_merge_stack. - change (a::l) with ([a]++l). rewrite app_assoc. etransitivity. + apply Permutation_app_tail. etransitivity. * apply Permutation_app_comm. * apply Permuted_merge_list_to_stack. + apply IHl. Qed.
imports: List Setoid Permutation Sorted Orders