case def_ X xs =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp
  exact h1
E : Env
σ : Instantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (def_ X xs))
no goals