Congruence rule for function application.
Proof 01. 1 ⊢ x = a, hypo. 02. 2 ⊢ y = b, hypo. 03. ⊢ f x y = f x y, eq_refl. 04. 1 ⊢ f x y = f a y, eq_subst 1 3, P t ↔ f x y = f t y. 05. 1, 2 ⊢ f x y = f a b, eq_subst 2 4, P t ↔ f x y = f a t. eq_cong_ii. ⊢ x = a → y = b → f x y = f a b, subj_intro_ii 5.
Dependencies
The given proof depends on two axioms:
eq_refl, eq_subst.