cases h1
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h1 : isFreeIn v phi ∨ isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
case inl
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h✝ : isFreeIn v phi
⊢ isFreeInInd v (phi.iff_ psi)

case inr
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
h✝ : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)