unfold sub
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi.not_)
E : Env
σ : Instantiation
τ : MetaInstantiation
phi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1 : IsMetaVarOrAllDefInEnv E phi
h2 : ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi).not_