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