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


DEBUG:Going to execute:
<coq-core.plugins.ltac::revert@0> $1
DEBUG LTAC Evaluated term: h