trunc_leq transparent & not an instance, no no-ops in trunc_contr

Also illustrates the fragility of universe annotations: changing the configuration of `IsTrunc` instances caused `ishprop_ooextendable` to take one fewer universe parameter.  Interestingly, results in a noticeable speedup, perhaps from smaller `IsTrunc` instances or fewer universes.
We should probably define `.+2` and `.+3`...