Require Export Image.

Implicit Arguments Im [[U] [V]].
Implicit Arguments Im_def [[U] [V]].
Implicit Arguments Im_add [[U] [V]].
Implicit Arguments image_empty [[U] [V]].
Implicit Arguments finite_image [[U] [V]].
Implicit Arguments Im_inv [[U] [V]].
Implicit Arguments not_injective_elim [[U] [V]].
Implicit Arguments cardinal_Im_intro [[U] [V]].
Implicit Arguments In_Image_elim [[U] [V]].
Implicit Arguments injective_preserves_cardinal [[U] [V]].
Implicit Arguments cardinal_decreases [[U] [V]].
Implicit Arguments Pigeonhole [[U] [V]].
Implicit Arguments Pigeonhole_principle [[U] [V]].