We prove the intermediate claim L1: 1 ∈ UnivOf (UnivOf Empty).

Apply ZF_ordsucc_closed to the current goal.

An exact proof term for the current goal is UnivOf_ZF_closed (UnivOf Empty).

An exact proof term for the current goal is ZF_closed_0 (UnivOf (UnivOf Empty)) (UnivOf Empty) (UnivOf_TransSet (UnivOf Empty)) (UnivOf_ZF_closed (UnivOf Empty)) (UnivOf_In (UnivOf Empty)).

An exact proof term for the current goal is MetaCatSet_terminal_gen (λX ⇒ X ∈ UnivOf (UnivOf Empty)) L1.