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