apply T_17_3
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))
case a.h1.h1
P : Formula
v t : VarName
Δ : Set Formula
h1 : fastAdmits v t P
h2 : IsDeduct Δ (fastReplaceFree v t P)
⊢ fastAdmits v t P