Theorem eq_trans

Proof
01. 1 ⊢ x = y, hypo.
02. 2 ⊢ y = z, hypo.
03. 1 ⊢ y = x, eq_symm 1.
04. 1, 2 ⊢ x = z, eq_subst 3 2, P u ↔ u = z.
eq_trans. ⊢ x = y → y = z → x = z, subj_intro_ii 4.

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