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