unfold IsMetaVarOrAllDefInEnv
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ IsMetaVarOrAllDefInEnv E true_
E : Env
σ : Instantiation
τ : MetaInstantiation
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ true_)
⊢ True