Notes

The proof of symmetry is worth to look at.
The definition of the impredicative leibniz equality leibniz 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 leibniz 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 leibniz_eq and eq_leibniz imply together that the propositions leibniz 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 leibniz 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, leibniz 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