n k (p : n <= k) (r : n = k) : p = r # leq_refl n. Proof. destruct p. + assert (c : idpath = r) by apply path_ishprop. destruct c. reflexivity. + destruct r^. contradiction (lt_irrefl _ p). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids