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