Lemma irrel_paths {X} (irr:∏ x y:X, x = y) {x y:X} (p q:x = y) : p = q. Proof. intros. assert (k : ∏ z:X, ∏ r:x = z, r @ irr z z = irr x z). { intros. induction r. reflexivity. } assert (l := k y p @ !k y q). apply (pathscomp_cancel_right _ _ _ l). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.