The Coq mailing list

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

Hi all,

Why this type error in the following sentences?

-------------------------------------
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.

(*
Error: In environment
H : nat = nat
The term "H" has type "nat = nat" while it is expected to have type
 "nat = nat".
*)
---------------------------------------

Thanks,
Jean-François