unfold IsMetaVarOrAllDefInEnv
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (pred_ X (List.map (↑σ) xs))
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ True