no goals
α✝ : Type u_1
a : α✝
acc : Array α✝
n✝ : Nat
⊢ insertNthTR.go a (n✝ + 1) [] acc = acc.data ++ insertNth (n✝ + 1) a []
simp [insertNthTR.go, insertNth]
no goals
α✝ : Type u_1
a✝ : α✝
acc : Array α✝
n : Nat
a : α✝
l : List α✝
⊢ insertNthTR.go a✝ (n + 1) (a :: l) acc = acc.data ++ insertNth (n + 1) a✝ (a :: l)
simp [insertNthTR.go, insertNth, insertNthTR_go_eq n l]