Goal:
  
  A : Type
  a : A
  l1 : list A
  IHl1 : ∀ (B : Type) (f : A → B) (l2 : list A),
           rev_map f (l1 ++ l2) = rev_map f l2 ++ rev_map f l1
  B : Type
  f : A → B
  l2 : list A
  ============================
   ((rev_map f l2 ++ rev_map f l1) ++ [f a] =
    (rev_map f l2 ++ rev_map f l1) ++ [f a])


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>