case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp
  tauto
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∪ {x}
no goals