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