We prove the intermediate claim L1: 0 ∈ UnivOf (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_initial_gen (λX ⇒ X ∈ UnivOf (UnivOf Empty)) L1.

∎