simp
case h1
P : Formula
u v : VarName
⊢ IsDeduct (∅ ∪ {exists_ u (forall_ v P)}) (forall_ v (exists_ u P))
case h1
P : Formula
u v : VarName
⊢ IsDeduct {exists_ u (forall_ v P)} (forall_ v (exists_ u P))