Pair acc lang regular

theorem pair_acc_lang_regular [Inhabited A] [h_fin : Finite M.State] {s s' : M.State} :    RegLang (M.PairAccLang acc s s') := by  let M' := (M.SingleInit s).addHist {False} (fun s a ↦ {s.2 ∨ s.1 ∈ acc})  use M', {p | p.1 = s' ∧ (p.2 ∨ s' ∈ acc) } ; constructor  · simp [M', NA.SingleInit] ; exact Finite.instProd  ext al ; constructor  · rintro ⟨n, as, ⟨ss', h_run', rfl, h_acc⟩, rfl⟩    have h_run := na_hist_fin_run_proj h_run'    use (Prod.fst ∘ ss')    constructor    · apply pair_path_fin_run.mpr ; simp [length_extract]      apply na_FinRun_modulo (hr := h_run)      · intro k h_k        have h1 : k < (as.extract 0 n).length := by simp [length_extract, h_k]        simp (disch := omega) [padDefault_elt_left h1, get_extract']      · simp    simp    obtain (h_acc | h_acc) := h_acc.symm    · use n ; simp [h_acc, length_extract]    by_contra! h_contra    suffices h : ∀ k < n + 1, ¬ (ss' k).2 by simp [h n (by omega)] at h_acc    intro k h_k ; induction' k with k h_ind    · have h_init := h_run'.1      simp [M', NA.addHist] at h_init      simp [h_init]    specialize h_ind (by omega)    specialize h_contra k (by simp [length_extract] ; omega)    have h_next := h_run'.2 k (by omega)    simp [M', NA.addHist, h_ind, h_contra] at h_next    simp [h_next]  · rintro ⟨ss, h_path, k0, h_k0, h_k0_acc⟩    use al.length, al.padDefault ; simp [extract_padDefault]    obtain ⟨h_run, rfl⟩ := pair_path_fin_run.mp h_path    have h_ne_init : Set.Nonempty {False} := by simp    have h_ne_next : ∀ (s : (M.SingleInit s).State × Prop) (a : A), Set.Nonempty {s.2 ∨ s.1 ∈ acc} := by simp    obtain ⟨hist, h_run'⟩ := na_hist_fin_run_exists h_ne_init h_ne_next h_run    use (fun k ↦ (ss k, hist k)) ; simp [M', h_run']    obtain (rfl | h_k0) := show k0 = al.length ∨ k0 < al.length by omega    · simp [h_k0_acc]    suffices h : ∀ k > k0, k < al.length + 1 → hist k by simp [h al.length h_k0]    intro k h_k    obtain ⟨j, rfl⟩ := show ∃ j, k = k0 + j + 1 by use (k - k0 - 1) ; omega    clear h_k ; induction' j with j h_ind    · have h_next := h_run'.2 k0 h_k0      simp [NA.addHist, h_k0_acc] at h_next      simp [h_next]    intro h_j    specialize h_ind (by omega)    have h_next := h_run'.2 (k0 + j + 1) (by omega)    simp [NA.addHist, h_ind] at h_next    simp [h_next, (show k0 + (j + 1) + 1 = k0 + j + 1 + 1 by omega)]