Omega Execution append

theorem OmegaExecution.append    (hmtr : lts.MTr s μl t) (hωtr : lts.OmegaExecution ss μs) (hm : ss 0 = t) :    ∃ ss', lts.OmegaExecution ss' (μl ++ω μs) ∧      ss' 0 = s ∧ ss' μl.length = t ∧ ss'.drop μl.length = ss := by  obtain ⟨sl, _, _, _, _⟩ := Execution.of_mTr hmtr  use sl.take μl.length ++ω ss  split_ands  · intro n    by_cases n < μl.length    · grind [get_append_left]    · by_cases n = μl.length      · grind [get_append_left, get_append_right']      · grind [get_append_right', hωtr (n - μl.length - 1)]  · grind [get_append_left]  · grind [get_append_left]  · grind [drop_append_of_ge_length]