proposition: Lemma Intersection_Empty A S0 : Same_set A (Intersection A (fun _ : A => False) S0) (fun _ => False).
proof: Proof. Ensembles_t. Qed.
imports: Fiat.Common.Ensembles.Notations Fiat.Common.Ensembles.Tactics Fiat.Common.Ensembles.Morphisms Fiat.Common