apply proof_imp_deduct
case a
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsDeduct Δ ((fastReplaceFree v t P).imp_ (exists_ v P))
case a.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))