proposition: Lemma treesort_twist1 : forall x y z t u:uniset, seq u (union y z) -> seq (union x (union u t)) (union (union y (union x t)) z).
proof: Proof. intros; apply seq_trans with (union x (union (union y z) t)). - apply seq_right; apply seq_left; trivial. - apply uniset_twist1. Qed.
imports: Bool Permut