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

...olable proof terms. As discussed in #454.
What precisely must a person who is familiar with the HoTT book figure out about Coq before they can understand this line? How many layers of stuff are piled on top of `concat`? Before it was straightworfward, now it's not.