apply isFreeInInd.exists_
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v (exists_ x phi)
case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ ¬v = x

case a
v x : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1_left : ¬v = x
h1_right : isFreeIn v phi
⊢ isFreeInInd v phi