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