apply deduction_theorem
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : ¬occursIn t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
h3 : ∀ H ∈ Δ, ¬isFreeIn t H
⊢ IsProof ((forall_ t (fastReplaceFree v t P)).imp_ (forall_ v (fastReplaceFree t v (fastReplaceFree v t P))))
case a.h1.h1
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)}) (forall_ v (fastReplaceFree t v (fastReplaceFree v t P)))