`fold`. Compared to the type of `fold`, the type of `ind` is more general as the kind of `p` is generalized from `Set` to `List a -> Set`, we call such `p` a *property* of the list. The second argument `step` for `ind` has an implicit term argument ``. The induction principle `ind` states that to prove a property `p` holds for any list `l`, one has to first prove that `Nil` has the property `p`, and then assuming `p` holds for any list `xs` as the induction hypothesis, prove that `p` holds for `Cons x xs` for any `x`.

We can now use the induction principle `ind` to prove that `map` behaves the same as the usual recursively defined `map’` (`lemma1`).

    map' : {a b : Set} -> (a -> b) -> List a -> List b
    map' f Nil = Nil
    map' f (Cons x xs) = Cons (f x) (map' f xs)

    lemma1 : {a b : Set} -> (f : a -> b) -> (l : List a) -> map f l == map' f l 
    lemma1 {a} {b} f l =  
       ind {a} {\ y -> map f y == map' f y} refl (\ 