The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Here is a version of "decidable equivalence relations -> excluded
middle" without setoid rewriting.

Require Import Relations.

Definition lem := forall p : Prop, p \/ ~p.

Definition decequiv :=
  forall (X : Type) (R : relation X),
    equiv X R -> forall x y, R x y \/ ~ (R x y).

Lemma small_lemma: forall p : Prop, p <-> (p <-> True).
Proof.
  tauto.
Qed.

Lemma decequiv_to_lem : decequiv -> lem.
Proof.
  intros D p.
  assert (E : equiv Prop iff).
  - firstorder.
  - destruct (D _ iff E p True); tauto.
Qed.

With kind regards,

Andrej