apply phi_ih h1_left
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ phi)
case left
E : Env
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih :
  IsMetaVarOrAllDefInEnv E phi →
    (∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ phi)
psi_ih :
  IsMetaVarOrAllDefInEnv E psi →
    (∀ X ∈ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)) → IsMetaVarOrAllDefInEnv E (sub σ τ psi)
h2 : ∀ (X : MetaVarName), X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet → IsMetaVarOrAllDefInEnv E (τ X)
h1_left : IsMetaVarOrAllDefInEnv E phi
h1_right : IsMetaVarOrAllDefInEnv E psi
⊢ ∀ X ∈ phi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)