Na concat fin run 0

theorem na_concat_fin_run_0 {m : ℕ} {as : Stream' A} {ss : Stream' (M0.Concat acc0 M1).State} :    (M0.Concat acc0 M1).FinRun m as ss ∧ (∃ s0, ss m = inl s0) ↔    (∃ ss0, M0.FinRun m as ss0 ∧ ∀ k < m + 1, ss k = inl (ss0 k)) := by  constructor  · rintro ⟨⟨h_init, h_next⟩, ⟨s0_m, h_s0_m⟩⟩    have h_all0 : ∀ k < m + 1, ∃ s0, ss k = inl s0 := by      by_contra h_contra      simp only [not_forall] at h_contra      obtain ⟨n, h_n, h_ss_n⟩ := h_contra      obtain ⟨s1, h_ss_n⟩ := not_M0_state h_ss_n      have h_contra : ∀ k < m - n + 1, ∃ s1, ss (k + n) = inr s1 := by        intro k h_k ; induction' k with k k_ind        · use s1 ; simpa        obtain ⟨s1', h_s1'⟩ := k_ind (by omega)        have h_next_k := h_next (k + n) (by omega)        simp [h_s1', NA.Concat] at h_next_k        obtain ⟨s1'', _, h_s1''⟩ := h_next_k        use s1'' ; rw [h_s1''] ; congr 1 ; omega      obtain ⟨s1_m, h_s1_m⟩ := h_contra (m - n) (by omega)      simp [(by omega: m - n + n = m), h_s0_m] at h_s1_m    choose ss0 h_ss0 using h_all0    use (fun k ↦ if h : k < m + 1 then ss0 k h else s0_m)    constructor <;> [constructor ; skip]    · simp [h_ss0 0 (by omega), NA.Concat] at h_init      simpa    · intro k h_k      have h_next_k := h_next k h_k      simp [h_ss0 k (by omega), h_ss0 (k + 1) (by omega), NA.Concat] at h_next_k      simpa [h_k, (by omega : k < m + 1)]    · intro k h_k ; simp [h_k, h_ss0 k h_k]  · rintro ⟨ss0, ⟨h_init0, h_next0⟩, h_ss0⟩    constructor <;> [constructor ; skip]    · simpa [h_ss0 0 (by omega), NA.Concat]    · intro k h_k      simp [h_ss0 k (by omega), h_ss0 (k + 1) (by omega), NA.Concat]      exact h_next0 k h_k    · use (ss0 m) ; exact h_ss0 m (by omega)