length (xs ++ ys) = length xs + length ys

total list_length_add : (xs, ys : List a) -> (length (xs ++ ys) = length xs + length ys)

Please log in; otherwise your solution and progress won't be saved