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 :: repeat f #|l| = f :: repeat f #|l|)


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| reflexivity
| symmetry; trivial
| contradiction
| congruence ]