SC
case a
P_r P_s : Formula
r s : VarName
P_u P_v : Formula
h1_1 : IsReplOfVarInFormula r s P_u P_v
h2 : ¬isBoundIn r P_u
h3 : ¬isBoundIn s P_u
h1_ih : IsProof ((eq_ r s).imp_ (P_u.iff_ P_v))
⊢ IsDeduct ∅
    (((eq_ r s).imp_ ((P_u.imp_ P_v).imp_ (P_v.imp_ P_u).not_).not_).imp_
      ((eq_ r s).imp_ ((P_u.not_.imp_ P_v.not_).imp_ (P_v.not_.imp_ P_u.not_).not_).not_))
no goals