{A : Type} (l l' : list A) : length (l ++ l') = (length l + length l')%nat. Proof. induction l as [|a l IHl] using list_ind. 1: reflexivity. simpl. exact (ap S IHl). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Require Import Types.Paths Types.Unit Types.Prod Types.Sigma Types.Sum