unfold sub at h1
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X (List.map (↑σ) xs))
⊢ IsMetaVarOrAllDefInEnv E (def_ X xs)