proposition: Lemma fillerEquation {X:Type} {x y z : X} {p : x = z} {q : y = z} (r : x = y) (k : r @ q = p) : @paths (∑ r, r@q=p) (r ,, k) ((p @ !q) ,, hornRotation_rr (idpath _)).
proof: Proof. apply proofirrelevancecontr. apply uniqueFiller. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics