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.
> it wouldn't ever actually be used

This isn't true.  Typeclass resolution will generally try `reflexivity`, so it'll only be used trivially, I think.