unfold IsMetaVarOrAllDefInEnv at h2
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : IsMetaVarOrAllDefInEnv [] (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)
E' : Env
h1 : ∃ E1, E' = E1 ++ []
X : DefName
xs : List VarName
h2 : ∃ d ∈ [], X = d.name ∧ xs.length = d.args.length
⊢ IsMetaVarOrAllDefInEnv E' (def_ X xs)