Map operation preserves list length

total map_preserves_length : (f : (a -> b)) -> (xs : List a) -> (length xs = length (map f xs))

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