In kernel/univ.ml, better allocation behavior, better eq_univs function
avoiding doing work twice, better leq not duplicating a Universe.equal
test.
Improve universe/level comparison using hashes.