An exact proof term for the current goal is (λX P ⇒ PowerI X (Sep X P) (Sep_Subq X P)).