Let n be given.
Assume H: nat_p n.
We will prove n ∈ {n ∈ UnivOf Empty|nat_p n}.
Apply SepI to the current goal.
We will prove n ∈ UnivOf Empty.
An exact proof term for the current goal is (nat_p_UnivOf_Empty n H).
We will prove nat_p n.
An exact proof term for the current goal is H.
∎