simp only [isFreeIn]
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬isFreeIn v (forall_ t (fastReplaceFree v t P))
case a.h1.h1.h2
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ ¬(¬v = t ∧ isFreeIn v (fastReplaceFree v t P))