simp only [predVarSet] at h1
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.not_.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_
τ : PredName → PredName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi.not_ = phi.not_