case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  tauto
P : PredName
n : ℕ
x : VarName
phi : Formula
phi_ih : predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
⊢ predVarOccursIn P n phi ↔ (P, n) ∈ phi.predVarSet
no goals