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

case not_
v : Var
a✝ : Formula
a_ih✝ : occursIn v a✝ ↔ v ∈ a✝.varSet
⊢ occursIn v a✝.not_ ↔ v ∈ a✝.not_.varSet

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

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