The Coq mailing list

["Patricia Peratto" <pperatto AT hotmail.com>]

I'm trying to define a rule for or_elim with dependent types

as follows:

 

(A,B:Prop; P:(A\/B->Set))
 ((a:A)(P (or_introl A B a)))
 ->((b:B)(P (or_intror A B b)))->(p:(A\/B))(P p)

 

with cases, but does not recognize p as formed

by constructors and asks type (P p) for the conclusion.

 

Is it not possible to define this rule in Coq?

 

Regards

 

Patricia Peratto