Let X, Y, Z, f, g, P, i0, i1 and copair be given.

Assume HP.

An exact proof term for the current goal is HP.

∎