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