The Coq mailing list

[T.Tsokos AT cs.bham.ac.uk]

Dear all, 

I am trying to do the following. Assuming I define 2 axioms:
Axiom first_axiom : forall (A: ...) ... .
Axiom second_axiom: forall (A: ...) ... .

Let's say I would like to define a construct of a natural number 
"embedding" the two properties described by the above axioms. Is there a 
way to do something like that (as if in sig, where the axioms provide a 
certificate):

Definition nat_embedded := {n:nat | first_axiom holds /\ second_axiom 
holds}.

so that I can prove properties on "nat_embedded" later on, that preserve 
the two axioms as well?

Thank you very much in advance. If it is a trivial aspect, please would you 
prompt me to some literature/references?

Regards,
Theo.