unfold Formula.metaVarSet at h2
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 ∈ (phi.imp_ psi).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))
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)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
h2 : ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (phi.imp_ psi))