simp only [fastAdmits] at h1
P : Formula
v t : VarName
h1 : fastAdmits v t P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsProof ((fastReplaceFree v t P).imp_ (exists_ v P))