apply IsAxiom.pred_2_ v v P
case a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ IsAxiom ((forall_ v P).imp_ P)
case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastAdmits v v P

case a.a.a
v : VarName
P : Formula
Δ : Set Formula
h1 : IsDeduct Δ (forall_ v P)
⊢ fastReplaceFree v v P = P