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


DEBUG:Going to execute:
induction m; simpl; rewrite ?app_length /=