To Single Accept language eq

@[scoped grind =]theorem toSingleAccept_language_eq {a : εNA.FinAcc State Symbol} :    language a.toSingleAccept = language a := by  ext xs  apply Iff.intro <;> intro h  case mp =>    rcases h with ⟨os, hos, os', hos', hsmtr⟩    rcases hos with ⟨s, hs₁, hs₂⟩    exists s    grind  case mpr =>    rcases h with ⟨s, hs, s', hs', hsmtr⟩    refine ⟨s, by grind, none, by grind, ?_⟩    rw [show xs.map some = xs.map some ++ [] by simp]    exact LTS.SMTr.comp (toSingleAccept_sMTr_sMTr.mpr hsmtr) <| LTS.SMTr.τ (LTS.STr.single hs')