simp only [def_exists_]
P : Formula
v t : VarName
h1 : fastAdmitsAux 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_ (forall_ v P.not_).not_)