coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: A strange theorem (Was: Can I define an equality dependent on another one?)

From: Benjamin Werner <Benjamin.Werner AT inria.fr>
To: sacerdot AT students.cs.unibo.it (Claudio Sacerdoti Coen)
Cc: blanqui AT lri.fr, coq-club AT pauillac.inria.fr
Subject: Re: A strange theorem (Was: Can I define an equality dependent on another one?)
Date: Tue, 5 Oct 1999 16:32:43 +0200 (MET DST)

Hi Claudio,

Yes, there is a problem here I was unaware of. To me it seems to be an
unexpected consequence of cumulativity.

I try to investigate a little before giving a more complete response.

Cheers,

Benjamin

A strange theorem (Was: Can I define an equality dependent on another one?), Claudio Sacerdoti Coen
- Re: A strange theorem (Was: Can I define an equality dependent on another one?), Benjamin Werner