apply isFreeInInd.iff_right_
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
case a
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v psi