Concat language eq

@[simp]theorem concat_language_eq {acc2 : Set State2} :    language (Buchi.mk (concat na1 na2) (inr '' acc2)) =    language na1 * language (Buchi.mk na2 acc2) := by  ext xs  constructor  · rintro ⟨ss, h_run, h_acc⟩    obtain ⟨k, h_k⟩ : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc]    obtain ⟨n, _, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_k    use xs.take n, h_acc1, xs.drop n, ?_, by simp    use ss2, h_run2    grind [(drop_frequently_iff_frequently n).mpr h_acc]  · rintro ⟨xs1, h_xs1, xs2, ⟨ss2, h_run2, h_acc2⟩, rfl⟩    obtain ⟨ss, h_run, h_map⟩ := concat_run_exists h_xs1 h_run2    use ss, h_run    apply (drop_frequently_iff_frequently xs1.length).mp    grind