rw [List.cons_append]
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: e ++ e₂) = subst σ (var v :: e) ++ subst σ e₂
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: (e ++ e₂)) = subst σ (var v :: e) ++ subst σ e₂