proposition: Lemma uniset_twist2 : forall x y z t:uniset, seq (union x (union (union y z) t)) (union (union y (union x z)) t).
proof: Proof. intros; apply seq_trans with (union (union x (union y z)) t). - apply seq_sym; apply union_ass. - apply seq_left; apply union_perm_left. Qed.
imports: Bool Permut