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