Lemma length_cons {A: UU} (x: A) (xs: list A) : length (x :: xs) = S (length xs). Proof. apply idpath. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.