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


DEBUG:Going to execute:
induction l1

Goals:
    A : Type
  ============================
   (∀ (B : Type) (f : A → B) (l2 : list A),
      rev_map f ([] ++ l2) = rev_map f l2 ++ rev_map f [])

  
  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 ((a :: l1) ++ l2) = rev_map f l2 ++ rev_map f (a :: l1))


DEBUG:Going to execute:
intros B f l2
DEBUG LTAC Evaluated term: l1