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:
reflexivity
DEBUG LTAC Evaluated term: rev_map_cons
DEBUG LTAC Evaluated term: rev_map_cons
DEBUG LTAC Evaluated term: rev_map_cons
DEBUG LTAC Evaluated term: rev_map_cons
DEBUG LTAC Evaluated term: IHl1
DEBUG LTAC Evaluated term: IHl1
DEBUG LTAC Evaluated term: app_assoc
DEBUG LTAC Evaluated term: app_assoc