The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.fr>]

>  Variable U:Type
>  Variable A:(Ensemble U)
> 
> Is there a way to define a new type such that only the elements of A
> has that type?
> 
> At first I thought that
> 
> Record A_T : Type :=
>   A_t {
>      A_element : U;
>      A_definition  : (In U A A_element)}
> 
> did it, but we want
> 
>   (a,b : A_T) a==b <-> (A_element a) == (A_element b)
> 
> and I don't want to assume this as an Axiom.

The last property is not provable since there are several proofs of
(In U A A_element) in general, and consequently it is not true that
dependent tuples are equal if their first projections are.

But your problem is a recurrent one. You can find related questions
and answers in the archive of the Coq mailing list at

        http://pauillac.inria.fr/coq/mailing-lists/coqclub/index.html

Among others, a particular discussion related to your problem is this one
initiated by Pierre Casteran:

        http://pauillac.inria.fr/coq/mailing-lists/coqclub/0167.html

I think that the answer Christine Paulin gave will answer your
question. I hope so...

Best regards,
-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr