proposition: Lemma indexed_to_family_union: IndexedUnion F = FamilyUnion ImageFamily.
proof: Proof. apply Extensionality_Ensembles. unfold Same_set. unfold Included. intuition. destruct H. apply family_union_intro with (F a). apply Im_intro with a. constructor. reflexivity. assumption. destruct H. destruct H. apply indexed_union_intro with x0. rewrite <- H1. assumption. Qed.
imports: Families Image ImageImplicit FiniteTypes EnsemblesTactics