apply deduction_theorem
P : Formula
u v : VarName
⊢ IsProof ((exists_ u (forall_ v P)).imp_ (forall_ v (exists_ u P)))
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {exists_ u (forall_ v P)}) (forall_ v (exists_ u P))