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

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