Theorem eq_cong

Congruence rule for function application.

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

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