x {xs} ih -> cong (Cons (f x)) ih) l

    refl : {a : Set} -> {x : a} -> x == x
    cong : {a b : Set} -> {m n : a} -> (f : a -> b) -> m == n -> f m == f n

In the proof of `lemma1`, we use a notion of equality `==` with the tactic `refl` to construct a reflexivity proof and the tactic `cong` to construct a congruence proof. The key to use the induction principle `ind` is to specify what kind of property on list we want to prove. In this case the property we have in mind is ` y -> map f y == map’ f y`. Thus the type of `ind ` is the following.

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

The first two arguments for the above type correspond to the base case and the step case in the inductive proof. For 