induction F
v : VarName
F : Formula
⊢ isFreeIn v F ↔ v ∈ F.freeVarSet
case pred_const_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_const_ a✝¹ a✝) ↔ v ∈ (pred_const_ a✝¹ a✝).freeVarSet

case pred_var_
v : VarName
a✝¹ : PredName
a✝ : List VarName
⊢ isFreeIn v (pred_var_ a✝¹ a✝) ↔ v ∈ (pred_var_ a✝¹ a✝).freeVarSet

case eq_
v a✝¹ a✝ : VarName
⊢ isFreeIn v (eq_ a✝¹ a✝) ↔ v ∈ (eq_ a✝¹ a✝).freeVarSet

case true_
v : VarName
⊢ isFreeIn v true_ ↔ v ∈ true_.freeVarSet

case false_
v : VarName
⊢ isFreeIn v false_ ↔ v ∈ false_.freeVarSet

case not_
v : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v a✝.not_ ↔ v ∈ a✝.not_.freeVarSet

case imp_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.imp_ a✝) ↔ v ∈ (a✝¹.imp_ a✝).freeVarSet

case and_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.and_ a✝) ↔ v ∈ (a✝¹.and_ a✝).freeVarSet

case or_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.or_ a✝) ↔ v ∈ (a✝¹.or_ a✝).freeVarSet

case iff_
v : VarName
a✝¹ a✝ : Formula
a_ih✝¹ : isFreeIn v a✝¹ ↔ v ∈ a✝¹.freeVarSet
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (a✝¹.iff_ a✝) ↔ v ∈ (a✝¹.iff_ a✝).freeVarSet

case forall_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (forall_ a✝¹ a✝) ↔ v ∈ (forall_ a✝¹ a✝).freeVarSet

case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isFreeIn v a✝ ↔ v ∈ a✝.freeVarSet
⊢ isFreeIn v (exists_ a✝¹ a✝) ↔ v ∈ (exists_ a✝¹ a✝).freeVarSet

case def_
v : VarName
a✝¹ : DefName
a✝ : List VarName
⊢ isFreeIn v (def_ a✝¹ a✝) ↔ v ∈ (def_ a✝¹ a✝).freeVarSet