apply
  IsDeduct.mp_
    (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsProof (P_U.iff_ P_V)
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ ((Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V)).imp_ (P_U.iff_ P_V))

case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (Forall_ ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList (U.iff_ V))