simp [List.add, List.length]
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length (x :: xs) = List.length (y :: ys) → List.length (add (x :: xs) (y :: ys)) = List.length (x :: xs)
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length xs = List.length ys → List.length (add xs ys) = List.length xs