rw [←Nat.add_one,
    Nat.add_assoc,
    Nat.add_comm (length cs),
    ←Nat.add_assoc]
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
as cs : List α
⊢ Nat.succ (length as + Nat.succ 0 + length cs) = length as + Nat.succ 0 + Nat.succ 0 + length cs
no goals