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