Let A and U be given.

Apply PowerI to the current goal.

Apply setminus_Subq to the current goal.

∎