apply IsDeduct.assume_
case h1.h1
P Q : Formula
v : VarName
⊢ IsDeduct {exists_ v (P.and_ Q)} (exists_ v (P.and_ Q))
case h1.h1.a
P Q : Formula
v : VarName
⊢ exists_ v (P.and_ Q) ∈ {exists_ v (P.and_ Q)}