Lemma length_one_back {A: UU} (l: list A) (l1: length l = 1): ∑ x: A, l = [x]. Proof. induction l. cbn in l1. induction (! l1). induction pr2 as [x xs]. exists x. induction xs. apply idpath. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Vectors.