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

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