{A : Type} {x y z : A} (p : x = z) (q : y = z) : (p @ q^) @ q = p := (match q as i return forall p, (p @ i^) @ i = p with idpath => fun p => match p with idpath => 1 end end) p.
Require Import Basics.Overture Basics.Tactics.