Definition cons' {x x' y z} (p : z ≤ y) (l : y < x') (e : x' = x) : z ≤ x. Proof. induction p as [n c]. exact (S n,,y,,x',,c,,l,,e). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.