Na pset run

theorem na_pset_run (as : Stream' A) (k : ℕ) :    M.PSet.DetRun as k = { s : M.State | ∃ ss, M.FinRun k as ss ∧ ss k = s } := by  induction' k with k h_ind  · rw [na_pset_reach_init as, Set.ext_iff]    intro s ; constructor    · intro h_init      use (fun k ↦ s) ; simpa [NA.FinRun]    · rintro ⟨ss, ⟨h_init, h_next⟩, h_s⟩      simpa [← h_s]  rw [na_pset_reach_next as k, h_ind, Set.ext_iff]  intro s ; constructor <;> simp  · rintro s' ⟨ss, ⟨h_init, h_next⟩, h_s'⟩ h_s    use (fun j ↦ if j < k + 1 then ss j else s)    simp ; constructor    · simpa    intro j h_j    rcases (by omega : j < k ∨ j = k) with h_j' | h_j'    · simp [h_j, h_j'] ; exact h_next j h_j'    · simpa [h_j', h_s']  · rintro ss ⟨h_init, h_next⟩ h_s    use (ss k)    simp [← h_s, h_next k (by omega)]    use ss ; simp ; constructor    · exact h_init    intro j h_j    exact h_next j (by omega)