Goal:
    A : Type  size : A → nat  l : list A
  ============================
   (list_size (rev l) = list_size l)


DEBUG:Going to execute:
induction l

Goals:
    A : Type  size : A → nat
  ============================
   (list_size (rev []) = list_size [])

  
  A : Type
  size : A → nat
  a : A
  l : list A
  IHl : list_size (rev l) = list_size l
  ============================
   (list_size (rev (a :: l)) = list_size (a :: l))


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l