We prove the intermediate claim L1: ∀X Y ∈ UnivOf (UnivOf Empty), X + Y ∈ UnivOf (UnivOf Empty).

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

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

∎