simp only [Formula.Forall_]
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))
case a
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList)