Let X, Y and f be given.
Assume Hf1 Hf2 Hf3.
We will
prove (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w).
Apply and3I to the current goal.
An exact proof term for the current goal is Hf1.
An exact proof term for the current goal is Hf2.
An exact proof term for the current goal is Hf3.