Normalization of El u
correctly print annotated equality
remove a catch-all case, tynorm-universe