apply Nat.succ.inj
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ length xs = length ys
case x
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ Nat.succ (length xs) = Nat.succ (length ys)