intro hsame
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length xs = List.length ys → List.length (add xs ys) = List.length xs
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
hsame : List.length xs = List.length ys
⊢ List.length (add xs ys) = List.length xs