Axiom. equi_subst
(A ↔ B) → P A → P B