proposition: Lemma length_sublist1 {A: UU} (l1: list A) (l2: list A) : length l1 ≤ length (l1 ++ l2).
proof: Proof. rewrite length_concatenate. apply natlehnplusnm. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe