proposition: Lemma Same_set__Intersection_beq__Setminus {A} (S0 : Ensemble A) f (b : bool) : Same_set _ (Intersection _ S0 (fun y => f y = b)) (Setminus _ S0 (fun y => f y = negb b)).
proof: Proof. Ensembles_t. Qed.
imports: Fiat.Common.Ensembles.Notations Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles.Morphisms Fiat.Common