return to top
source
Proves various lemmas about List.insertIdx.
List.insertIdx
Erasing nth element of a list, then inserting a at the same place is the same as setting nth element to a.
n
a
We assume that n ≠ length l, because otherwise LHS equals l ++ [a] while RHS equals l.
n ≠ length l
l ++ [a]
l
Erasing an index commutes with List.map.
List.map