case def_ X xs =>
  unfold IsMetaVarOrAllDefInEnv at h1
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp
  exact h1
E : Env
σ : Instantiation
τ : MetaInstantiation
X : DefName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (def_ X xs)
h2 : ∀ X_1 ∈ (def_ X xs).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (def_ X xs))
no goals