proposition: Lemma length_zero_back {A: UU} (l: list A): length l = 0 → l = [].
proof: Proof. revert l. refine (list_ind _ _ _). - reflexivity. - intros x xs _ HP. apply negpathssx0 in HP. contradiction. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe