Let X, Y, Z, f, g, P, pi0, pi1 and pair be given.

Assume HP.

An exact proof term for the current goal is HP.

∎