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

...olable proof terms. As discussed in #454.
I think this is a showstopper, if `simpl` can't simplify `idpath @ idpath`.  Why on earth?