Definition card_le := [n:nat][X:Type] 
  (ExT [f:nat->X] ((x:X) (ExT [i:nat] (lt i n) /\ ((f i) == x)))).

Definition card_ge := [n:nat][X:Type]
  (ExT [f:X->nat] ((i:nat) (lt i n) -> (ExT [x:X] ((f x) == i)))).

Definition card_eq := [n:nat][X:Type]
  (ExT [f:nat->X] (ExT [g:X->nat] ((x:X) ((f (g x)) == x) /\ (lt (g x) n)))).

Definition finite := [X:Type] (ExT [n:nat] (card_le n X)).

Definition inf_card_le := [n:nat][X:Type] 
  (sigT ? [f:nat->X] ((x:X) (sigT ? [i:nat] (lt i n) /\ ((f i) == x)))).

Definition inf_finite := [X:Type] (sigT ? [n:nat] (inf_card_le n X)).