Theorem: FOL.NV.isFreeIn_iff_isFreeInInd (FOL/NV/Binders.lean)

State before:
v : VarName
F : Formula
⊢ isFreeIn v F ↔ isFreeInInd v F
Tactic:
constructor
State after:
case mp
v : VarName
F : Formula
⊢ isFreeIn v F → isFreeInInd v F

case mpr
v : VarName
F : Formula
⊢ isFreeInInd v F → isFreeIn v F

State before:
case mp
v : VarName
F : Formula
⊢ isFreeIn v F → isFreeInInd v F
Tactic:
exact isFreeIn_imp_isFreeInInd v F
State after:
no goals

State before:
case mpr
v : VarName
F : Formula
⊢ isFreeInInd v F → isFreeIn v F
Tactic:
exact isFreeInInd_imp_isFreeIn v F
State after:
no goals