∀ {α : Type u_1} (l : List α) (x : α) (i j : ℕ),
  i ≤ j →
    ∀ (i_1 : ℕ) (h : i_1 < (List.take i (l.insertIdx j x)).length) (h₂ : i_1 < (List.take i l).length),
      (List.take i (l.insertIdx j x))[i_1] = (List.take i l)[i_1]