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