rw [subst_append, subst_tr _ _ e]
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst (subst.trans σ σ') e = subst σ' (σ v ++ subst σ e)
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst σ' (subst σ e) = subst σ' (σ v) ++ subst σ' (subst σ e)