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