simp only [subst, List.append_eq]
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ subst σ (const c :: e₁ ++ e₂) = subst σ (const c :: e₁) ++ subst σ e₂
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: subst σ (e₁ ++ e₂) = const c :: subst σ e₁ ++ subst σ e₂