Let pb, pi0, pi1 and pair be given.

Assume HP.

An exact proof term for the current goal is HP.

∎