apply isFreeInInd.not_
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi.not_
case a
v : VarName
phi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
h1 : isFreeIn v phi
⊢ isFreeInInd v phi