the base case, we just need `refl`. For the step case, the induction hypothesis `ih` has the type `map f xs == map’ f xs`, we just need to show `map f (Cons x xs) == Cons (f x) (map’ f xs)`. Since `map f (Cons x xs)` can be evaluated to `Cons (f x) (map f xs)`, we finish the proof by a congruence on the induction hypothesis, so `cong (Cons (f x)) ih` is the proof for `map f (Cons x xs) == Cons (f x) (map’ f xs)`.

To summarize, the fold functions for *regular* data types (i.e. non-nested inductive data types such as `List` and `Nat`) are well-behaved in the following sense. (1) The fold functions are defined by well-founded recursion. (2) The fold functions can be used to define a range of terminating functions (including maps). (3) The types of the fold functions can be generalized to the corresponding induction principles. Unfortunately, these properties of folds for regular data types does not directly carry over to nested data types. Consider the following nested data type.

    data Bush (a : Set) : Set where
      NilB : Bush a
      ConsB :  a -> Bush (Bush a) -> 