rw [subst_append ..]
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: subst σ (e₁ ++ e₂) = const c :: subst σ e₁ ++ subst σ e₂
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: (subst σ e₁ ++ subst σ e₂) = const c :: subst σ e₁ ++ subst σ e₂