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

...olable proof terms. As discussed in #454.
@andrejbauer just reverting this line is not possible.
I made a new commit, hopefully more readable.

On Mon, Sep 8, 2014 at 12:08 AM, Andrej Bauer <notifications@github.com>
wrote:

> In contrib/HoTTBook.v:
>
> > @@ -69,7 +69,7 @@ Definition Book_2_1_1 := @HoTT.Overture.inverse.
> >  (* ================================================== lem:concat *)
> >  (** Lemma 2.1.2 *)
> >
> > -Definition Book_2_1_2 := @HoTT.Overture.concat.
> > +Definition Book_2_1_2 := (fun A => (@transitivity _ (@paths A))).
> >
>
> 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.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17217727>.
>