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

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

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

case h1.h1.h4
P : Formula
u v : VarName
⊢ ¬isFreeIn u (exists_ u P)