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