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

...olable proof terms. As discussed in #454.
I think if we can't fake `@concat` then there is no point to defining `atconcat`; if someone has to know to write `atconcat` instead of `@concat` then they might as well write `@transitivity` instead.