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


DEBUG:Going to execute:
induction l

Goals:
    A : Type  size : A → nat  l' : list A
  ============================
   (list_size ([] ++ l') = list_size [] + list_size l')

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


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