Goal:
    A : Type  B : Type  f : B  l : list A
  ============================
   ((fix map (l : list A) : list B :=
       match l with
       | [] => []
       | _ :: t => f :: map t
       end) l = repeat f #|l|)


DEBUG:Going to execute:
induction l; cbn
DEBUG LTAC Evaluated term: map_map