Let A, B and f be given.
Assume Hf.
Let U be given.
Assume HU.
Apply PowerI to the current goal.
Let y be given.
Let x be given.
rewrite the current goal using H1 (from left to right).
Apply Hf to the current goal.
Apply PowerE A U HU to the current goal.
An exact proof term for the current goal is Hx.
∎