proposition: Corollary isweqpathscomp0r' {X : UU} (x : X) {x' x'' : X} (e' : x' = x'') : isweq (λ e : x = x', e @ e').
proof: Proof. intros p. use tpair. exists (p @ !e'). now apply hornRotation_rr. cbn. intros [q l]. apply fillerEquation. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics