Using the standard (type class based) transitivity tactic for more contr...

...olable proof terms. As discussed in #454.
@spitters, if you include the `Notation`s I gave for `@concat`, `@Overture.concat`, and `@HoTT.Overture.concat`, then reverting this line is possible.  Of course, then the line is somewhat of a deception, and you have to trace the usage of the notation.