simp only [occursIn]
case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ occursIn v (exists_ a✝¹ a✝)
case exists_
v a✝¹ : VarName
a✝ : Formula
a_ih✝ : isBoundIn v a✝ → occursIn v a✝
h1 : v = a✝¹ ∨ isBoundIn v a✝
⊢ v = a✝¹ ∨ occursIn v a✝