An exact proof term for the current goal is (λX : set ⇒ PowerI X Empty (Subq_Empty X)).