unfold sub at h1
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)
⊢ IsMetaVarOrAllDefInEnv E phi.not_
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E (sub σ τ phi) → IsMetaVarOrAllDefInEnv E phi
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ phi).not_
⊢ IsMetaVarOrAllDefInEnv E phi.not_