intro hsame
y : ℤ
ys : List ℤ
⊢ List.length [] = List.length (y :: ys) → List.length (add [] (y :: ys)) = List.length []
y : ℤ
ys : List ℤ
hsame : List.length [] = List.length (y :: ys)
⊢ List.length (add [] (y :: ys)) = List.length []