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