unfold IsMetaVarOrAllDefInEnv
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E true_
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E true_
h2 : ∀ X ∈ true_.metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ True