{A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : (p @ q) @ r = p @ (q @ r) := match r with idpath => match q with idpath => match p with idpath => 1 end end end.
Require Import Basics.Overture Basics.Tactics.