{A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : p = r^ @ q -> r @ p = q. Proof. destruct r. intro h. exact (concat_1p _ @ h @ concat_1p _). Defined.
Require Import Basics.Overture Basics.Tactics.