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

...olable proof terms. As discussed in #454.
Yeah, that sounds about right.  I mean, if you want to update `coq-scripts` to whatever the newest version is, feel free, but I'd prefer it done in its own commit and not bundled like this.