Loop run one iter

theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} {k : ℕ}    (h : na.loop.Run xs ss) (h1 : 0 < k) (h2 : (ss k).isLeft) :    ∃ n, n ≤ k ∧ xs.take n ∈ language na - 1 ∧ na.loop.Run (xs.drop n) (ss.drop n) := by  have h1' : ∃ k, 0 < k ∧ (ss k).isLeft := by grind  let n := Nat.find h1'  have : 0 < n ∧ (ss n).isLeft := Nat.find_spec h1'  have : ∀ k, 0 < k → k < n → (ss k).isRight := by grind [Nat.find_min h1']  refine ⟨n, by grind, ⟨?_, ?_⟩, ?_⟩  · grind [loop_run_left_right_left]  · have neq : (ωSequence.take n xs).length ≠ 0 := by grind    exact neq.imp (congrArg List.length)  · grind [loop_run_from_left]