rw [List.get_of_eq (l.concat_eq_append a)]
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (List.concat l a) { val := i, isLt := h } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a