The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to make the following code work?  It currently says "Error: Not the right number of induction arguments." on the last line.

Require Import List.

Functional Scheme fold_right_rect := Induction for fold_right Sort Type.

Goal forall x ls, fold_right and x ls -> x.

Proof.

  intros x ls H.

  functional induction H using fold_right_rect.

Thanks,

Jason