proposition: Lemma subfamily_intersection: forall F G:Family T, Included F G -> Included (FamilyIntersection G) (FamilyIntersection F).
proof: Proof. unfold Included. intros. constructor. destruct H0. intros. apply H0. apply H. assumption. Qed.
imports: Ensembles EnsemblesImplicit