The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

Consider the following:

Require Import List.

Record rec  : Type := mk_rec

  { t           : Type;            

    stateset    : list t 

  }.

Inductive t' : Type :=  

  | A: t'.

Parameter P: t' -> Prop.

Example test:

  forall b, b = mk_rec t' (A::A::A::nil) ->

   forall e, In e (@stateset b) -> P e.

Proof.

I cannot type the above lemma, as I get

Error: In environment

b : rec

e : t b

The term "e" has type "t b" while it is expected to have type "t'".

but t b, is actually equal to t'.. how can I make it work?

Cheers.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.