cases 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))
h3 : ¬isBoundIn s (forall_ x P_u)
h2 : r ≠ x ∧ ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))
case intro
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))
h3 : ¬isBoundIn s (forall_ x P_u)
left✝ : r ≠ x
right✝ : ¬isBoundIn r P_u
⊢ IsProof ((eq_ r s).imp_ ((forall_ x P_u).iff_ (forall_ x P_v)))