Na loop fin run exists

theorem na_loop_fin_run_exists {n : ℕ} {as : Stream' A} {ss' : Stream' M.State}    (h_run' : M.FinRun n as ss') (h_acc' : ss' n ∈ acc) :    ∃ ss, (M.Loop acc).FinRun n as ss ∧ ss n = inl () ∧ (∀ k < n, k > 0 → ss k = inr (ss' k)) := by  rcases (show n = 0 ∨ n > 0 by omega) with ⟨rfl⟩ | h_n  · use (fun k ↦ inl ()) ; simp [NA.FinRun, NA.Loop]  let ss k := if k = 0 ∨ k = n then inl () else inr (ss' k)  suffices h : ∃ ss', M.FinRun n as ss' ∧ ss' n ∈ acc ∧ ss 0 = inl () ∧ ss n = inl () ∧ (∀ k < n, k > 0 → ss k = inr (ss' k)) by    obtain ⟨h_run, h_ss_n, _⟩ := (na_loop_fin_run h_n).mpr h    use ss ; simp [h_run, h_ss_n]    intro k h_k_n h_k_0 ; simp [ss] ; omega  use ss' ; simp [h_run', h_acc', ss] ; omega