The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

More generally, is the following set of declaration consistent with
CIC + Classical ?


Parameter the : forall (A:Set)(P:A->Prop)
              (E : exists a, P a)(U : forall a b, P a -> P b  -> a = b) , A.

Axiom the_ok : forall A P E U, P (the A P E U).
Axiom the_eq : forall (A:Set) (P:A->Prop) E U a, P a -> a = the A P E U.

Pierre

-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.