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