induction F
v : Var
F : Formula
⊢ occursIn v F ∧ v.isBound ↔ v ∈ F.boundVarSet
case pred_
v : Var
a✝¹ : String
a✝ : List Var
⊢ occursIn v (pred_ a✝¹ a✝) ∧ v.isBound ↔ v ∈ (pred_ a✝¹ a✝).boundVarSet

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ∧ v.isBound ↔ v ∈ a✝.boundVarSet
⊢ occursIn v a✝.not_ ∧ v.isBound ↔ v ∈ a✝.not_.boundVarSet

case imp_
v : Var
a✝¹ a✝ : Formula
a_ih✝¹ : occursIn v a✝¹ ∧ v.isBound ↔ v ∈ a✝¹.boundVarSet
a_ih✝ : occursIn v a✝ ∧ v.isBound ↔ v ∈ a✝.boundVarSet
⊢ occursIn v (a✝¹.imp_ a✝) ∧ v.isBound ↔ v ∈ (a✝¹.imp_ a✝).boundVarSet

case forall_
v : Var
a✝¹ : String
a✝ : Formula
a_ih✝ : occursIn v a✝ ∧ v.isBound ↔ v ∈ a✝.boundVarSet
⊢ occursIn v (forall_ a✝¹ a✝) ∧ v.isBound ↔ v ∈ (forall_ a✝¹ a✝).boundVarSet