Proof 01. 1 ⊢ inj f X Y, hypo. 02. 1 ⊢ map f X Y, lsubj_conj_eliml inj_equi 1. inj_is_map. ⊢ inj f X Y → map f X Y, subj_intro 2.