proposition: Lemma Intersection_associative {X : Type} (U V W: Ensemble X) : Intersection (Intersection U V) W = Intersection U (Intersection V W).
proof: Proof. now extensionality_ensembles. Qed.
imports: EnsemblesImplicit EnsemblesTactics