apply IsDeduct.axiom_
case a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsDeduct ∅ ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)
case a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ IsAxiom ((forall_ v P.not_).imp_ (fastReplaceFree v t P).not_)