simp at a1
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H ∈ {P.imp_ (forall_ v Q)}
⊢ ¬isFreeIn v H
case h1.h2
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
H : Formula
a1 : H = P.imp_ (forall_ v Q)
⊢ ¬isFreeIn v H