no goals
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublistsLen (length (a :: l)) (a :: l) = [a :: l]
simp only [length, sublistsLen_succ_cons, sublistsLen_length, map,
  sublistsLen_of_length_lt (lt_succ_self _), nil_append]