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