proposition: Lemma sub_indexed_intersection: forall {A B T:Type} (f:A->B) (F:IndexedFamily B T), let subF := (fun a:A => F (f a)) in Included (IndexedIntersection F) (IndexedIntersection subF).
proof: Proof. unfold Included. intros. constructor. destruct H. intro. apply H. Qed.
imports: Families Image ImageImplicit FiniteTypes EnsemblesTactics