Let po, i0, i1 and copair be given.

Assume HP.

An exact proof term for the current goal is HP.

∎