Fin Concat language eq

theorem finConcat_language_eq [Inhabited Symbol] :    language (FinAcc.mk (finConcat na1 na2) (inr '' (some '' na2.accept))) =    language na1 * language na2 := by  ext xl  constructor  · rintro ⟨s, _, t, h_acc, h_mtr⟩    obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.extend_omegaExecution h_mtr    have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run]    have hr : (ss xl.length).isRight := by grind    obtain ⟨n, _, _, ss2, h_run2, _⟩ := concat_run_proj hc hr    refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩    · grind [totalize_language_eq, take_append_of_le_length]    · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind