proposition: Lemma Union_assoc {A} (x y z : Ensemble A) : (x ∪ (y ∪ z)) ≅ ((x ∪ y) ∪ z).
proof: Proof. Ensembles_t. Qed.
imports: Fiat.Common.Ensembles.Notations Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles.Morphisms Fiat.Common