apply T_17_4 P v v Δ
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (exists_ v P)
case h1
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ fastAdmits v v P

case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (fastReplaceFree v v P)