proposition: Lemma empty_indexed_union: forall {T:Type} (F:IndexedFamily False T), IndexedUnion F = Empty_set.
proof: Proof. intros. apply Extensionality_Ensembles; red; split; red; intros. destruct H. destruct a. destruct H. Qed.
imports: Families Image ImageImplicit FiniteTypes EnsemblesTactics