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