{A : Type} {x y z : A} {p p' p'' : x = y} {q q' q'' : y = z} (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') : (a @@ c) @ (b @@ d) = (a @ b) @@ (c @ d). Proof. case d. case c. case b. case a. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.