unfold Formula.metaVarSet at h1
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.not_.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_
σ : Instantiation
τ τ' : MetaInstantiation
phi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
h1 : phi.metaVarSet = ∅
⊢ sub σ τ phi.not_ = sub σ τ' phi.not_