Let X, Y and Z be given.

Assume H1 H2.

Apply H1 to the current goal.

Let f be given.

Assume H3: bij X Y f.

Apply H2 to the current goal.

Let g be given.

Assume H4: bij Y Z g.

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

We use (λx : set ⇒ g (f x)) to witness the existential quantifier.

An exact proof term for the current goal is bij_comp X Y Z f g H3 H4.

∎