The Coq mailing list

[Nicolas Marti <nicolas AT yl.is.s.u-tokyo.ac.jp>]

Try it that way:

Theorem fold_folded : forall (A:Set) (xs:list A) (f:A -> A -> A) (a:A),
    folded A f a xs (fold A f a xs).
Proof.
  induction xs; simpl; intro.
  constructor.
  constructor.
  intuition.
Qed.

When you make an induction over a variable, assure to put it leftmost
in the lemma definition/type. To understand why, just look at 

Check list_rect.

which is (nearby) the induction principle you invoke.


      Nicolas