Let X, Y and f be given.

Assume H1 H2.

We will prove (∀x ∈ X, f x ∈ Y) ∧ (∀x z ∈ X, f x = f z → x = z).

Apply andI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

∎