Concat run proj

theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} {k : ℕ}    (hc : (concat na1 na2).Run xs ss) (hr : (ss k).isRight) :    ∃ n, n ≤ k ∧ xs.take n ∈ language na1 ∧    ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by  have hr' : ∃ k, (ss k).isRight := by grind  let n := Nat.find hr'  have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr' h_k  refine ⟨n, by grind, ?_, ?_⟩  · by_cases h_n : n = 0    · grind [concat_start_right]    · grind [concat_run_left_right]  · exact concat_run_right hc n hl (Nat.find_spec hr')