proposition: Lemma Same_set_Intersection_Union' {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