simp only [List.length] at h
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length (x :: xs) = length (y :: ys)
⊢ length xs = length ys
α : Type u_1
β : Type u_2
x : α
xs : List α
y : β
ys : List β
h : length xs + 1 = length ys + 1
⊢ length xs = length ys