Axiom eq_subst

Axiom. eq_subst
x = y → P x → P y

The substitution schema for equality.