Let X and Y be given.

Assume H1.

Apply H1 to the current goal.

Let f be given.

Assume Hf: bij X Y f.

We will prove ∃f : set → set, inj X Y f.

We use f to witness the existential quantifier.

An exact proof term for the current goal is bij_inj X Y f Hf.

∎