Definition lengthN {A : Type} (xs : list A) : N :=
  N.of_nat (length xs).
