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