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