induction ((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)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) ((U.freeVarSet ∪ V.freeVarSet) ∩ P_U.boundVarSet).toList)
case a.nil
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) [])

case a.cons
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tail✝)
⊢ IsDeduct ∅ (List.foldr forall_ (U.iff_ V) (head✝ :: tail✝))