Require Export Image.

Arguments Im {U} {V}.
Arguments Im_def {U} {V}.
Arguments Im_add {U} {V}.
Arguments image_empty {U} {V}.
Arguments finite_image {U} {V}.
Arguments Im_inv {U} {V}.
Arguments not_injective_elim {U} {V}.
Arguments cardinal_Im_intro {U} {V}.
Arguments In_Image_elim {U} {V}.
Arguments injective_preserves_cardinal {U} {V}.
Arguments cardinal_decreases {U} {V}.
Arguments Pigeonhole {U} {V}.
Arguments Pigeonhole_principle {U} {V}.
