proposition: Lemma FiniteT_nat_cardinal_False: FiniteT_nat_cardinal False empty_finite = 0.
proof: Proof. apply FiniteT_nat_cardinal_cond. assert (@Full_set False = @Empty_set False). apply Extensionality_Ensembles; red; split; auto with sets. red; intros. destruct x. rewrite H. constructor. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality