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


DEBUG:Going to execute:
t; easy