Apply nat_ind to the current goal.
We will prove 0 ∈ UnivOf Empty.
An exact proof term for the current goal is (UnivOf_In Empty).
Let n be given.
Assume Hn: nat_p n.
Assume IHn: n ∈ UnivOf Empty.
We will prove ordsucc n ∈ UnivOf Empty.
An exact proof term for the current goal is (ZF_ordsucc_closed (UnivOf Empty) (UnivOf_ZF_closed Empty) n IHn).
∎