refactor(library/definitional/util): cleanup
feat(library/definitional/util): add telescope equality for HoTT library

This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.