proposition: Lemma irrel_paths {X} (irr:∏ x y:X, x = y) {x y:X} (p q:x = y) : p = q.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics