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