exact h1_ih h2_right h3_right
case h1.a.a.h1.a.h1
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_left : r ≠ x
h2_right : ¬isBoundIn r P_u
h3_left : s ≠ x
h3_right : ¬isBoundIn s P_u
⊢ IsDeduct ∅ ((eq_ r s).imp_ (P_u.iff_ P_v))
no goals