simp only [isBoundIn] at h2
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬isBoundIn r (forall_ x P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
P_r P_s : Formula
r s x : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_ih : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h2 : ¬(r = x ∨ isBoundIn r P_u)
h3 : ¬isBoundIn s (forall_ x P_u)
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))