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

Apply ZF_ordsucc_closed to the current goal.

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

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

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