The Coq mailing list

[Victor Porton <porton AT narod.ru>]

In Carlos Simpson's ZF theory there was used = instead of <-> for the reason 
mentioned in the following comment:

axioms.v:

(*** the following axioms can be obtained from the Ensembles library but we 
include it here
as an axiom; it is used for convenience, allowing us to replace iff by 
equality so as to
be able to rewrite using equality of propositions 
**********************************)

(***) Axiom iff_eq : forall P Q : Prop, (P -> Q) -> (Q -> P) -> P = Q.

Jose Grimm's GAIA inherited this mode of expressing equality for 
propositions, as his work was based on the work of Carlos Simpson.

Now there exists:

Require Import Setoid.

It allows rewrite to work with <->.

Now we need to make a decision: Should we switch to using Setoid from 
standard library and replace every = comparing propositions with <->?

Please all interested parties make a comment.

Also: If we'll decide to replace all such occurrences of = with <-> who will 
do the job of searching all occurrences? I may do it gradually replacing only 
these occurrences which I may encountered on my way of doing a derived 
theory. (It may be somehow hard for me, I'm yet weak in imperative proofs 
scripts as I instead decided to learn the declarative proof mode.)

-- 
Victor Porton - http://portonvictor.org