apply IsAxiom.pred_2_ v v P P
case a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsAxiom ((forall_ v P).imp_ P)
case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ fastAdmits v v P

case a.a.a
P : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ fastReplaceFree v v P = P