Definition hornRotation_lr {X:Type} {x y z : X} {p : x = z} {q : y = z} {r : x = y} : q = (!r) @ p ≃ r @ q = p. Proof. induction p, r; cbn. apply idweq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.