unfold sub
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (τ X)