apply generalization
case h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} (forall_ u P)
case h1.h1.h1
P : Formula
u v : VarName
⊢ IsDeduct {forall_ u (forall_ v P)} P

case h1.h1.h2
P : Formula
u v : VarName
⊢ ∀ H ∈ {forall_ u (forall_ v P)}, ¬isFreeIn u H