proposition: Lemma Same_set__Intersection_Complement__Setminus {A} (S0 S1 : Ensemble A) : Same_set _ (Intersection _ S0 (Complement _ S1)) (Setminus _ S0 S1).
proof: Proof. Ensembles_t. Qed.
imports: Fiat.Common.Ensembles.Notations Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles.Morphisms Fiat.Common