Remove an ununsed pattern and commented code in the kernel.
Reestablish completeness in conversion when Opaque primitive
projections are used.
Change reduction_of_red_expr to return an e_reduction_function returning
an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.