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