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

case a.a.a
P : Formula
v t : VarName
h1 : fastAdmitsAux v t ∅ P
⊢ fastReplaceFree v t P.not_ = (fastReplaceFree v t P).not_