Acc lang loop concat

theorem acc_lang_loop_concat :    ((M.Loop acc).AcceptedLang {inl ()}) * ((M.Loop acc).AcceptedLang {inl ()}) ⊆    (M.Loop acc).AcceptedLang {inl ()} := by  rintro al ⟨al1, al2, ⟨n1, as1, ⟨ss1, h_run1, h_acc1⟩, rfl⟩, ⟨n2, as2, ⟨ss2, h_run2, h_acc2⟩, rfl⟩, rfl⟩  use (n1 + n2), ((as1.extract 0 n1) ++ₛ as2) ; symm ; constructor  · have h1 : (as1.extract 0 n1).length ≤ n1 + n2 := by simp [length_extract]    simp [extract_append_zero_right h1, length_extract]  let ss k := if k < n1 then ss1 k else ss2 (k - n1)  use ss ; symm ; constructor  · simp at h_acc2 ; simp [ss, h_acc2]  constructor  · suffices h_0 : ss 0 = inl () by simp [h_0, NA.Loop]    rcases (show n1 = 0 ∨ n1 > 0 by omega) with h_n1 | h_n1 <;> simp [ss, h_n1]    · exact h_run2.1    · exact h_run1.1  intro k h_k  rcases (show k + 1 < n1 ∨ k + 1 = n1 ∨ k + 1 > n1 by omega) with h_k | h_k | h_k  · have h1 : k < (as1.extract 0 n1).length := by simp [length_extract] ; omega    simp (disch := omega) [get_append_left' h1, get_extract']    have h_next := h_run1.2 k (by omega)    simp [ss, h_next, h_k, (show k < n1 by omega)]  · have h_next := h_run1.2 k (by omega)    suffices h_n1 : ss2 0 = ss1 (k + 1) by      have h1 : k < (as1.extract 0 n1).length := by simp [length_extract] ; omega      simp (disch := omega) [get_append_left' h1, get_extract']      simp [ss, ← h_k, h_n1, h_next]    simp [← h_k] at h_acc1    simp [h_acc1] ; exact h_run2.1  · have h_next := h_run2.2 (k - n1) (by omega)    have h1 : (as1.extract 0 n1).length ≤ k := by simp [length_extract] ; omega    simp [get_append_right' h1, length_extract, ss, h_next,      (show ¬ k + 1 < n1 by omega), (show ¬ k < n1 by omega), (show k + 1 - n1 = k - n1 + 1 by omega)]