The Coq mailing list

[Jean-François Dufourd <jfd AT unistra.fr>]

Thanks, Julien. It works with Set in place of Type in:

Theorem subst: forall(T U:Set), T = U -> T -> U.
Proof.
   intros. rewrite <-H. apply X.
Defined.

But how can I achieve the proof of:

Require Import Arith.

Lemma test_subst: forall H : nat = nat,
   subst nat nat H 5 = 5.
?

Thank you,
Regards,

Jean-François


Le 27/10/2014 13:05, 
julien.forest AT ensiie.fr
 a écrit :
> On Sun, 26 Oct 2014 16:29:18 +0100
> Jean-François Dufourd 
> <jfd AT unistra.fr>
>  wrote:
>
> > Theorem subst: forall(T U:Type), T = U -> T -> U.
> > Proof.
> >    intros. rewrite <-H. apply X.
> > Defined.
> >
> > Require Import Arith.
> >
> > Lemma test_subst: forall H : nat = nat,
> >    subst nat nat H 5 = 5.
>
> Hi,
> your hypothesis H has exact type @eq Set nat nat while the subst Lemma
> waits for an hypothesis (@eq Type nat nat). The conversion between Set
> and Type does not seems to be automatic here.
>
> Best regards,
>
> Julien