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