case forall_ _ phi phi_ih =>
  simp only [occursIn]
  simp only [varSet]
  exact phi_ih
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v (forall_ a✝ phi) ↔ v ∈ (forall_ a✝ phi).varSet
no goals