apply IsDeduct.mp_ (forall_ t (fastReplaceFree v t P))
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))

case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsDeduct Δ (forall_ t (fastReplaceFree v t P))