cases h1
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : ¬v = x ∧ isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
case intro
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
left✝ : ¬v = x
right✝ : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)