The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

ohpato wrote:
> Mr. Bertot, 
>
> Thank you for the kind answers and advice.
>
>
>
>   
Don't thank me too much, I got the name of various types wrong, so that 
my message
may have been a little confusing.
> Yves Bertot wrote:
>   
> > ohpato wrote:
> >     
> > ....
> > This property is probably wrong, as soon as your type Record_T contains 
> > two distinguishable elements (elements f1 and f2 such that f1 <> f2), 
> > you can construct two elements of Record_ID that share the same first 
> > component and have different second components, these records are 
> > provably different.  If you add this property as an axiom, you will get 
> > an inconsistent logic, this kills the purpose of using a proof system.
> >     
In this sentence, Record_T should have been Field_T, and Record_ID 
should have been
Record_T...

My mistake,

Yves