fact: Definition concat_p_pp {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.
imports: Basics.Overture Basics.Tactics