unfold IsMetaVarOrAllDefInEnv
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
⊢ IsMetaVarOrAllDefInEnv E (pred_ X xs)
E : Env
σ : Instantiation
τ : MetaInstantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (pred_ X xs))
⊢ True