Theorem f_equal

Proof
01. 1 ⊢ x = y, hypo.
02. ⊢ f x = f x, eq_refl.
03. 1 ⊢ f x = f y, eq_subst 1 2, P u ↔ f x = f u.
f_equal. ⊢ x = y → f x = f y, subj_intro 3.

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