The Coq mailing list

[richard <richard.dapoigny AT univ-smb.fr>]

Dear Coq user,

I am working on sets with characteristic functions and a datatype called object for wich equality is decidable.

Singletons called ι are also defined in this context. An excerpt of the code is given below.

Definition object: Type := t.

Definition eqobject_dec := eq_dec.

Inductive N : Type :=
    | Caract  : (object -> Prop) -> N.

Definition caract (s :N)(a:object) : Prop := let (f) := s in f a.
Definition In (s :N)(a:object) : Prop := caract s a = True.
Definition incl (s1 s2 :N) := forall a:object, In s1 a -> In s2 a.
Definition set_eq (s1 s2 :N) := forall a:object, In s1 a = In s2 a.

Definition ι (a:object) :=
  Caract
    (fun a':object =>
       match eqobject_dec a a' with
       | left h => True
       | right h => False
       end).

My question is the following : is there a possibility to prove the pairing axiom with these assumptions, i.e.  to prove that 

Lemma pairN : forall (x:object)(A:N), set_eq (ι x) A <-> ι x = A.

In addition we assume classical logic.

Thanks in advance,

Richard