Na loop fin run

theorem na_loop_fin_run {n : ℕ} {as : Stream' A} {ss : Stream' (M.Loop acc).State} (h : n > 0) :    (M.Loop acc).FinRun n as ss ∧ ss n = inl () ∧ (∀ k < n, k > 0 → ss k ∈ range inr) ↔    ∃ 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  constructor  · rintro ⟨⟨h_init, h_next⟩, h_inl_n, h_inr⟩    simp [NA.Loop] at h_init    rcases (show n = 1 ∨ n > 1 by omega) with h_n | h_n    · obtain ⟨rfl⟩ := h_n      specialize h_next 0 (by omega)      simp [h_init, h_inl_n, NA.Loop] at h_next      obtain ⟨s0, h_s0, s1, h_acc, h_next⟩ := h_next      use (fun k ↦ if k = 0 then s0 else if k = 1 then s1 else s0)      simp [h_init, h_acc, h_inl_n, NA.FinRun, h_s0, h_next]    · obtain ⟨s1, h_s1⟩ := h_inr 1 h_n (by omega)      have h_next_0 := h_next 0 h      simp [h_init, ← h_s1, NA.Loop] at h_next_0      obtain ⟨s0, h_s0, h_next_0⟩ := h_next_0      obtain ⟨sn1, h_sn1⟩ := h_inr (n - 1) (by omega) (by omega)      have h_next_n1 := h_next (n - 1) (by omega)      have h_n1 : n - 1 + 1 = n := by omega      simp [h_n1, h_inl_n, ← h_sn1, NA.Loop] at h_next_n1      obtain ⟨sn, h_sn, h_next_n1⟩ := h_next_n1      have h_ss' : ∀ k, k > 0 → k < n → ∃ ss', ss k = inr ss' := by        intro k h_k_0 h_k_n        obtain ⟨s', h_s'⟩ := h_inr k h_k_n h_k_0        use s' ; simp [h_s']      choose ss' h_ss' using h_ss'      use (fun k ↦ if h0 : k = 0 then s0 else if hn : k < n then ss' k (by omega) hn else if k = n then sn else s0)      simp [(show n ≠ 0 by omega), h_init, h_inl_n, h_sn, NA.FinRun, h_s0]      constructor      · intro k h_k_n        rcases (show k = 0 ∨ k = n - 1 ∨ k > 0 ∧ k < n - 1 by omega) with h_k_0 | h_k_n' | ⟨h_k_0, h_k_n'⟩        · obtain ⟨rfl⟩ := h_k_0          have h_ss_1 := h_ss' 1 (by omega) (h_n)          rw [← h_s1, inr.inj_iff] at h_ss_1          simp [h_n, ← h_ss_1, h_next_0]        · obtain ⟨rfl⟩ := h_k_n'          have h_ss_n1 := h_ss' (n - 1) (by omega) h_k_n          rw [← h_sn1, inr.inj_iff] at h_ss_n1          simp [(show n - 1 + 1 = n by omega), (show n - 1 ≠ 0 by omega), h, ← h_ss_n1, h_next_n1]        · have h_ss_k := h_ss' k h_k_0 h_k_n          have h_ss_k1 := h_ss' (k + 1) (by omega) (by omega)          have h_next_k := h_next k h_k_n          simp [h_ss_k, h_ss_k1, NA.Loop] at h_next_k          simp [(show k + 1 < n by omega), (show k ≠ 0 by omega), h_k_n, h_next_k]      · intro k h_k_n h_k_0        simp [h_k_n, h_k_0, (show k ≠ 0 by omega), h_ss']  · rintro ⟨ss', ⟨h_init, h_next⟩, h_acc, h_inl_0, h_inl_n, h_inr⟩    constructor <;> [constructor ; constructor]    · simp [h_inl_0, NA.Loop]    · intro k h_k_n      rcases (show k = 0 ∨ k > 0 by omega) with h_k_0 | h_k_0      · specialize h_next 0 h        rcases (show n = 1 ∨ n > 1 by omega) with h_n | h_n        · obtain ⟨rfl⟩ := h_n          simp [h_k_0, h_inl_0, NA.Loop, h_inl_n]          use (ss' 0) ; simp [h_init] ; use (ss' 1)        · specialize h_inr 1 h_n (by omega)          simp [h_k_0, h_inl_0, NA.Loop, h_inr]          use (ss' 0)      · specialize h_next k (h_k_n)        have h_ss_k := h_inr k h_k_n h_k_0        rcases (show k + 1 < n ∨ k = n - 1 by omega) with h_k_n' | h_k_n'        · have h_ss_k' := h_inr (k + 1) h_k_n' (by omega)          simpa [h_ss_k, h_ss_k', NA.Loop]        · obtain ⟨rfl⟩ := h_k_n'          have h_n1 : n - 1 + 1 = n := by omega          simp [h_n1] at h_next          simp [h_n1, h_ss_k, h_inl_n, NA.Loop]          use (ss' n)    · exact h_inl_n    · intro k h_k_n h_k_0      simp [h_inr k h_k_n h_k_0]