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