The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I discovered that replacing "intros []" with "intro r; dependent destruction r" fixes things, if I [Require Import Program].

-Jason

On Mon, May 28, 2012 at 6:31 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Thanks!

However, if I replace [T a] with [T a a] in the definition of [f], then the second proof fails; on "intros []", I get 

Error: Illegal application (Type Error): 

The term "f" of type

 "forall (T : Type -> Type -> Type) (a : Type), T a a -> Prop"

cannot be applied to the terms

 "T" : "Type -> Type -> Type"

 "b" : "Type"

 "x0" : "T a b"

The 3rd term has type "T a b" which should be coercible to 

"T b b".

-Jason

On Mon, May 28, 2012 at 4:47 PM, gallais @ ensl.org <guillaume.allais AT ens-lyon.org> wrote:

Parameter f : forall T (a : Type), T a -> Prop.

Implicit Arguments f [T a].

Inductive g T (a : Type) : forall (b : Type) (x : T a b), Prop :=
 | injf : forall (t : T a a), f t -> g T a a t.

Implicit Arguments g [T a b].

Theorem g_ne T (a b : Type) (x : T a b) : a <> b -> ~g x.

 intros H gx ; inversion gx ; contradiction.
Qed.

Theorem f_eq_g T (a : Type) (x : T a a) : f x <-> g x.

split.
 intro fx ; constructor ; assumption.
 intros [] ; firstorder.
Qed.