Theorem eq_symm

Proof
01. 1 ⊢ x = y, hypo.
02. 1 ⊢ y = x, eq_subst 1 eq_refl, P u ↔ u = x.
eq_symm. ⊢ x = y → y = x, subj_intro 2.

Dependencies
The given proof depends on two axioms:
eq_refl, eq_subst.