Let X and Y be given.

Apply PowerEq X Y to the current goal.

An exact proof term for the current goal is (λH _ ⇒ H).

∎