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