Acc lang union

theorem acc_lang_union :    (NA.Sum M).AcceptedLang (NA.Sum_Acc M acc) = ⋃ i : I, (M i).AcceptedLang (acc i) := by  ext al ; simp [NA.Sum_Acc, NA.AcceptedLang, NA.FinAccept]  constructor  · rintro ⟨n, as, ⟨ss, h_run, h_acc⟩, h_al⟩    obtain ⟨i, ss_i, h_run_i, h_ss_i⟩ := na_sum_fin_run.mp h_run    use i, n, as    constructor    · use ss_i      constructor      · assumption      obtain ⟨i', si', h_si', h_last⟩ := h_acc      simp [h_ss_i] at h_last      rw [Sigma.mk.inj_iff] at h_last      obtain ⟨rfl, h_si'_eq⟩ := h_last      rw [heq_eq_eq] at h_si'_eq      simpa [← h_si'_eq]    · assumption  · rintro ⟨i, n, as, ⟨ss_i, h_run, h_last⟩, h_al⟩    use n, as    constructor    · use ((Sigma.mk i) ∘ ss_i)      constructor      · apply na_sum_fin_run.mpr        use i, ss_i        simp [h_run]      · use i, ss_i (Fin.last n)        simpa    · assumption