The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

> I suspect I need K (or I am just too stupid). Can anybody conform  
> either? I.e. can I prove this using Coq.Logic.Eqdep or without?

I am just too stupid. But so is Coq. I just need to use dependent  
inversion.

Actually I realized that I can prove it with the standard eliminator  
for equality:

eq_elim : forall (A:Set)(x:A)(P:forall y:A, (x=y)->Set)
                            (m:P x (refl_equal x))
                            (y:A)(p:x=y),P y p.

This is not automatically derived by Coq (why not?) but it can be  
proven using dependent inversion. It seems that you always get in  
trouble if you try to use dependent types in Coq.

I attach my completed Russell derivation.

Cheers,
Thorsten


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

Attachment: l16-crib.v
Description: Binary data