apply h2
case right
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 : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ IsMetaVarOrAllDefInEnv E (τ X)
case right.a
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 : MetaVarName
a1 : X ∈ psi.metaVarSet
⊢ X ∈ phi.metaVarSet ∨ X ∈ psi.metaVarSet