simp only [sub]
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ sub σ meta_var_ (sub σ' meta_var_ (def_ X xs)) = sub (σ.comp σ') meta_var_ (def_ X xs)
σ σ' : Instantiation
X : DefName
xs : List VarName
⊢ def_ X (List.map (↑σ) (List.map (↑σ') xs)) = def_ X (List.map (↑(σ.comp σ')) xs)