Omega Execution flatten m Tr

theorem OmegaExecution.flatten_mTr [Inhabited Label]    {ts : ωSequence State} {μls : ωSequence (List Label)}    (hmtr : ∀ k, lts.MTr (ts k) (μls k) (ts (k + 1))) (hpos : ∀ k, (μls k).length > 0) :    ∃ ss, lts.OmegaExecution ss μls.flatten ∧ ∀ k, ss (μls.cumLen k) = ts k := by  choose sls h_sls using fun k ↦ Execution.of_mTr (hmtr k)  obtain ⟨ss, h_ss, h_seg⟩ := OmegaExecution.flatten_execution h_sls hpos  use ss, h_ss  intro k  have : ss.extract (μls.cumLen k) (μls.cumLen (k + 1)) ≠ [] := by grind  have h1 : 0 < (ss.extract (μls.cumLen k) (μls.cumLen (k + 1))).length :=    List.length_pos_iff.mpr this  grind [List.getElem_of_eq (h_seg k) h1]