Acc lang pset

theorem acc_lang_pset :    M.PSet.toNA.AcceptedLang (M.PSet_Acc acc) = M.AcceptedLang acc := by  ext al ; simp only [NA.AcceptedLang, NA.FinAccept] ; constructor  · rintro ⟨n, as, ⟨ss', h_run', h_acc'⟩, h_al⟩    have h_sn' := da_fin_run_unique h_run' n (by omega)    rw [na_pset_run] at h_sn'    simp [h_sn', NA.PSet_Acc] at h_acc'    obtain ⟨sn, ⟨ss, h_run, h_sn⟩, h_acc⟩ := h_acc'    use n, as ; simp [h_al]    use ss ; simp [h_run, h_sn, h_acc]  · rintro ⟨n, as, ⟨ss, h_run, h_sn⟩, h_al⟩    use n, as ; simp [h_al]    use (M.PSet.DetRun as) ; constructor    · apply da_fin_run_exists    · rw [na_pset_run, NA.PSet_Acc]      use (ss n) ; simp [h_sn] ; use ss