simp only [subst]
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst (subst.trans σ σ') (var v :: e) = subst σ' (subst σ (var v :: e))
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst (subst.trans σ σ') e = subst σ' (σ v ++ subst σ e)