The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi Adam,

That was great! Thanks a million. Using chapter 9 from your book I  
could now finish the proof. For posteriority's sake, the completed  
script is below. By the way, are these axioms about equality  
implementable? Or does extraction become impossible when one of these  
axioms is used?

Require Import Arith.
Require Import Omega.
Require Import JMeq.
Require Import Eqdep.

Inductive T : nat -> Set :=
 | MkT  : forall (n:nat), T n
 | MkT2 : forall (n:nat), T n.

Variable U : nat.

Definition a : T U := MkT U.

Lemma foo : U = U + 1 - 1.
Proof.
 omega.
Qed.

Definition b : T (U + 1 - 1).
Proof.
 rewrite <- foo.
 exact (MkT U).
Defined.

Lemma a_is_b : JMeq a b.
Proof.
  cbv beta delta -[minus plus].
  generalize foo.
  rewrite <- foo.
  intros.
  rewrite (UIP_refl _ _ e).
  apply JMeq_refl.
Qed.

Inductive X : forall (n:nat), T n -> Set := .

Lemma bar : X (U + 1 - 1) b = X U a.
Proof.
  generalize a_is_b.
  generalize b.
  rewrite <- foo.
  intros.
  rewrite H.
  reflexivity.
Qed.

Edsko