proposition: Lemma union_ass : forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
proof: Proof. unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z; auto with bool. Qed.
imports: Bool Permut