The Coq mailing list

[julien.forest AT ensiie.fr]

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