proposition: Lemma list_tail_cons {A: UU} (x: A) (xs: list A) : tail (x :: xs) = ii1 xs.
proof: Proof. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe