The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

T.Tsokos AT cs.bham.ac.uk
 wrote:
> 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?

It is puzzling that you bother to maintain proofs that the axioms hold 
for particular natural numbers, when you have already asserted that the 
axioms hold for all naturals.  With the axioms in place, we can prove 
that [nat_embedded] is isomorphic to [nat].