case pred_ X xs =>
  simp only [sub]
  unfold Instantiation.comp
  simp
σ σ' : Instantiation
X : PredName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (pred_ X xs)) = sub (σ.comp σ') meta_var_ (pred_ X xs)
no goals