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.