Definition hornRotation_rl {X:Type} {x y z : X} {p : x = z} {q : y = z} {r : x = y} : p @ !q = r ≃ p = r @ q. Proof. induction q, r; cbn. apply eqweqmap. apply (maponpaths (λ k, k = idpath x)). apply pathscomp0rid. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.