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

...olable proof terms. As discussed in #454.
Ok, I think this particular line should just be reversed, that's all. The "correct" answer is that `Book_2_1_2` is precisely `concat`, and not some instance of transitivity.