Definition cons1 {n y z z'} : ∏ (x : X) (e : z = z') (l : z' < y) (c : chain n y x), chain (S n) z x. Proof. induction n as [|n H]. - intros x e l c. exact (z',,y,,e,,l,,c). - intros x e l c. induction c as [s [t [c' [l' e']]]]. exact (s,,t,,H s e l c',,l',,e'). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.