We prove the intermediate claim L1: ∀X Y ∈ UnivOf Empty, X ⨯ Y ∈ UnivOf Empty.

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

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

∎