case pred_ X xs =>
  unfold sub
  unfold IsMetaVarOrAllDefInEnv
  simp only
E : Env
σ : Instantiation
X : PredName
xs : List VarName
h1 : IsMetaVarOrAllDefInEnv E (pred_ X xs)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (pred_ X xs))
no goals