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

...olable proof terms. As discussed in #454.
@spitters, this works fine for me:
```coq
Notation concat := (transitivity (R := @paths _)) (only parsing).
(** We fake the [@concat] notation. The [format] specifiers are left in so we get reasonable printing if we ever decide to remove the [only parsing]. *)
(* Notation taken from ssreflect's ssrfun. *)
Notation "@ 'concat' A" := (@transitivity _ (@paths A) _)
                             (only parsing, at level 10, A at level 8, format "@ 'concat'  A").
Notation "@ 'Overture.concat' A" := (@transitivity _ (@paths A) _)
                             (only parsing, at level 10, A at level 8, format "@ 'Overture.concat'  A").
Notation "@ 'HoTT.Overture.concat' A" := (@transitivity _ (@paths A) _)
                             (only parsing, at level 10, A at level 8, format "@ 'HoTT.Overture.concat'  A").
Infix "@" := (@transitivity _ _ _ _ _ _) (at level 20).
```