proposition: Lemma length_concatenate {A: UU} (l1: list A) (l2: list A) : length (l1 ++ l2) = length l1 + length l2.
proof: Proof. revert l1. apply list_ind. - apply idpath. - intros x xs IH. change (S (length (xs ++ l2)) = S (length xs + length l2)). apply maponpaths. apply IH. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe