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).

∎