The Coq mailing list

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

Dear Coq users,

Assuming classical logic with the following definitions:

Variable object : Set. (* elements *)

Definition eqobject := @Logic.eq object.

Lemma eqobject_dec : forall x y:object, eqobject x y \/ ~(eqobject x y).
Proof.
intros x y;unfold eqobject;apply classic.
Qed.

Is there a way to transform the following definition with Prop in classical logic (i.e., to remove booleans since left and right refer to sumbool):

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

Thanks for your help.