Let X and U be given.

Assume HUsub.

Apply PowerI X U HUsub to the current goal.

∎