The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

(* The script below works with 8.2pl3 but reports "Error: Unbound and
 * ungeneralizable variable A" with 8.3rc1 *)

Inductive list (A:Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.
Implicit Arguments nil [A].
Implicit Arguments cons [A].
Infix "::" := cons (at level 60, right associativity).
Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) 
-> False.
  intros.
  induction b.
  inversion H.
  inversion H. apply IHb in H2.
  auto.
  Defined.