Overlooked to remove a change in kernel/closure that made reducing under
a primitive projection impossible.
Better handling of the universe context in case of Admitted proof obligations.