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