simp
case h2
U V P_U P_V : Formula
h1 : IsReplOfFormulaInFormula U V P_U P_V
h2 : IsProof (U.iff_ V)
hd : VarName
tl : List VarName
ih : IsDeduct ∅ (List.foldr forall_ (U.iff_ V) tl)
⊢ ∀ H ∈ ∅, ¬isFreeIn hd H
no goals