An exact proof term for the current goal is (λn H ⇒ SepE2 (UnivOf Empty) nat_p n H).