Goal:
    A : Type  f : nat → A  m : nat
  ============================
   (#|unfold m f| = m)


DEBUG:Going to execute:
induction m

Goals:
    A : Type  f : nat → A
  ============================
   (#|unfold 0 f| = 0)

    A : Type  f : nat → A  m : nat  IHm : #|unfold m f| = m
  ============================
   (#|unfold (S m) f| = S m)


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

Goals:
    A : Type  f : nat → A
  ============================
   (0 = 0)

    A : Type  f : nat → A  m : nat  IHm : #|unfold m f| = m
  ============================
   (#|unfold m f ++ [f m]| = S m)


DEBUG:Going to execute:
rewrite ?app_length /=