Acc lang concat e

theorem acc_lang_concat_e :    (M0.Concat acc0 M1).AcceptedLang (inl '' acc0) = M0.AcceptedLang acc0 := by  ext al ; constructor  · rintro ⟨m, as, ⟨ss, h_run, h_acc⟩, h_al⟩    have h_m : ∃ s0, ss m = inl s0 := by      obtain ⟨s0, _, h_s0⟩ := h_acc      use s0 ; simp [h_s0]    obtain ⟨ss0, h_run0,h_ss0⟩ := na_concat_fin_run_0.mp ⟨h_run, h_m⟩    use m, as ; simp [h_al]    use ss0 ; simp [h_run0]    obtain ⟨sm, h_sm_acc, h_sm⟩ := h_acc    rw [h_ss0 m (by omega), inl.inj_iff] at h_sm    simpa [← h_sm]  · rintro ⟨m, as, ⟨ss0, h_run0, h_acc0⟩, h_al⟩    use m, as ; simp [h_al]    let ss : Stream' (M0.Concat acc0 M1).State := inl ∘ ss0    use ss ; constructor    · suffices (M0.Concat acc0 M1).FinRun m as ss ∧ (∃ s0, ss m = inl s0) by tauto      apply na_concat_fin_run_0.mpr      use ss0 ; simp [h_run0]      intro k h_k ; simp [ss]    · simp [ss] ; use (ss0 m)