proposition: Lemma FiniteT_nat_cardinal_cond: forall (X:Type) (H:FiniteT X) (n:nat), cardinal _ (@Full_set X) n -> FiniteT_nat_cardinal X H = n.
proof: Proof. intros. pose proof (FiniteT_has_nat_cardinal X H). destruct H1. red in H1. destruct H1. transitivity x. symmetry; apply H2. apply FiniteT_nat_cardinal_def. apply H2; trivial. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality