apply Nat.succ_lt_succ
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ Nat.succ (length xs) < Nat.succ (Nat.succ (length xs))
case a.a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
⊢ length xs < length xs + 1