simp only [isBoundIn] at h2
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬isBoundIn r (P_u.imp_ Q_u)
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))
P_r P_s : Formula
r s : VarName
P_u Q_u P_v Q_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h1_2 : IsReplOfVarInFormula r s Q_u Q_v
h1_ih_1 : ¬isBoundIn r P_u → ¬isBoundIn s P_u → IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
h1_ih_2 : ¬isBoundIn r Q_u → ¬isBoundIn s Q_u → IsProof ((eq_ r s).imp_ (Q_u.iff_ Q_v))
h2 : ¬(isBoundIn r P_u ∨ isBoundIn r Q_u)
h3 : ¬isBoundIn s (P_u.imp_ Q_u)
⊢ IsProof ((eq_ r s).imp_ ((P_u.imp_ Q_u).iff_ (P_v.imp_ Q_v)))