The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  I'm referring to the axioms at http://coq.inria.fr/cocorico/CoqAndAxioms

  I would like to use:

== BEGIN ==

Axiom func_ext_dep : forall (A:Type) (B:A->Type) (f g : forall x, B x),
  (forall x, f x = g x) -> f = g.

Axiom prop_ext : forall (P Q : Prop),
  (P <-> Q) -> P = Q.

Axiom classic : forall (P : Prop), P \/ ~ P.

== END ==

  as they would greatly simplify the proofs / tactics I'm using.
However, I'm unsure if I can do this because:

I don't know if:

(1) the three above together is known to be consistent.
(2) the three above together is known to be inconsistent.
(3) neither (1) or (2) is known, but it's okay in the community to use
all three together.

By "okay" -- I mean if I were to submit a paper using the three axioms
above, would people consider my proofs invalid because I used them.
(In particular, I don't need them, but func/prop ext greatly
simplifies rewrite rules.)

Thanks!