Totalize run mtr

theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (Option State)} {n : ℕ}    (h : na.totalize.Run xs ss) (hl : (ss n).isSome) :    ∃ s t, na.MTr s (xs.take n) t ∧ s ∈ na.start ∧ ss 0 = some s ∧ ss n = some t := by  obtain ⟨s, _, eq₁⟩ := h.start  obtain ⟨t, eq₂⟩ := isSome_iff_exists.mp hl  use s, t  refine ⟨?_, by grind⟩  -- TODO: `grind` does not use congruence relations with `na.totalize.MTr`  rw [← LTS.totalize.nonsink_mtr_iff, ← extract_eq_take, eq₁, ← eq₂]  exact LTS.OmegaExecution.extract_mTr h.trans (by grind)