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