Let T and T' be given.

Assume H.

An exact proof term for the current goal is H.

∎