proposition: Lemma FiniteT_has_nat_cardinal: forall X:Type, FiniteT X -> exists! n:nat, cardinal _ (@Full_set X) n.
proof: Proof. intros. apply -> unique_existence; split. apply finite_cardinal. pose (idX := fun x:X => x). assert (Im Full_set idX = Full_set). apply Extensionality_Ensembles. red; split. red; intros; constructor. red; intros. exists x. constructor. trivial. rewrite <- H0. apply FiniteT_img with (f:=fun x:X => x). assumption. intros. case (finite_eq_dec X H y1 y2); tauto. red; intros. apply cardinal_unicity with X Full_set; trivial. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description FunctionalExtensionality