An exact proof term for the current goal is MetaCatSet_initial_gen (λ_ ⇒ True) TrueI.