Let X, Y and Z be given.

Assume H1 H2.

Apply H1 to the current goal.

Let f be given.

Assume Hf: inj X Y f.

Apply H2 to the current goal.

Let g be given.

Assume Hg: inj Y Z g.

We will prove ∃h : set → set, inj X Z h.

Set h to be the term λx ⇒ g (f x) of type set → set.

We use h to witness the existential quantifier.

An exact proof term for the current goal is inj_comp X Y Z f g Hf Hg.

∎