case meta_var_ X =>
  unfold Formula.metaVarSet at h2
  simp at h2
  unfold sub
  exact h2
E : Env
σ : Instantiation
τ : MetaInstantiation
X : MetaVarName
h1 : IsMetaVarOrAllDefInEnv E (meta_var_ X)
h2 : ∀ X_1 ∈ (meta_var_ X).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X_1)
⊢ IsMetaVarOrAllDefInEnv E (sub σ τ (meta_var_ X))
no goals