## Notes

The proof of symmetry is worth to look at.

The definition of the impredicative leibniz equality
`impredicative_eq a b` has an asymmetric form, due to
the implication `P a -> P b `, but the symmetry is
restored by a proper substitution for `P` :

Let us assume `impredicative_eq a b`, *i.e.*
H : forall P:A->Prop, P a -> P b

Then for every predicate `Q` over `A`,
the term `H fun a0:A => Q a0 -> Q a` is a proof of the proposition :
(Q a -> Q a)-> Q b -> Q a

from which we trivially prove `Q b -> Q a`

The theorems `impredicative_eq_eq`
and `eq_impredicative_eq` imply together that
the propositions `impredicative_eq a b` and
`a=b` are *logically* equivalent. Nevertheless, there is a
slight diffrence. There is a constant `eq_rec` which allows
to rewrite `a` in `b` in a construction of sort `Set` ,
but you can't do that with the proposition
`impredicative_eq a b`.

In other words, you can't build a term of the following type :
forall (x : A) (P:A->Set), P x -> (forall y:A, impredicative_eq x y-> P y

The same problem remains if one replaces `Set` with `Type` and
`eq_rec` with `eq_rect`.

Going home

Pierre Castéran