The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

If, for some reason, you can't recast the inductive definition, you
could also use the following:

Definition map {A B:Type} (f:A->B) (l:List A) : List B :=
List_rect (fun A' _ => A = A' -> List B)
  (fun _ _ => nil B)
  (fun A' (a:A') (l':List A') (recval: A=A' -> List B)
     (e: A = A') =>
   cons B
     (f (match e in (_ = T) return (T -> A) with
         | eq_refl => fun a' => a'
         end a))
     (recval e))
  A l (eq_refl A).

The fundamental idea here is that P A' l reduces to "A = A' -> List
B", and then you use the equality hypothesis to cast a from type A' to
A.

As you can probably see, rewriting the inductive definition as
guillaume suggested is much simpler...
-- 
Daniel Schepler