The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm trying to prove the following lemma, and getting an error on [Qed].

Lemma eqType2Set (a b : Set) : @eq Type a b -> @eq Set a b.

  intro; subst; reflexivity.

Qed.

Coq says

Error: Illegal application (Type Error): 

The term "eq" of type "forall A : Type, A -> A -> Prop"

cannot be applied to the terms

 "Set" : "Type"

 "a0" : "Type"

 "b" : "Set"

The 2nd term has type "Type" which should be coercible to 

"Set".

If I [Set Printing All] and [Show Proof], Coq tells me that the proof is 

(fun (a b : Set) (H : @eq Type a b) =>

 @eq_ind_r Type b (fun a0 : Type => @eq Set a0 b) (@eq_refl Set b) a H)

Does anyone have ideas/suggestions for how to make this proof go through?  Does it need an axiom?

-Jason