Definition inductionOnFiller {X:Type} {x y z:X} (p:x=z) (q:y=z) (S := λ r:x=y, r @ q = p) (T : ∏ r (e : S r), Type) (t : T (p @ !q) (hornRotation_rr (idpath _))) : ∏ (r:x=y) (e : r @ q = p), T r e. Proof. intros. use (transportPathTotal _ t). apply pathsinv0. apply fillerEquation. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.