intro v a1
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ ∀ (v : VarName),
    (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U → v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
v : VarName
a1 : (isFreeIn v U ∨ isFreeIn v V) ∧ isBoundIn v P_U
⊢ v ∈ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList