insertIdx #
Proves various lemmas about List.insertIdx
.
Alias of List.insertIdx_zero
.
Alias of List.insertIdx_succ_nil
.
Alias of List.insertIdx_succ_cons
.
Alias of List.length_insertIdx
.
Alias of List.eraseIdx_insertIdx
.
Alias of List.eraseIdx_insertIdx
.
Alias of List.insertIdx_eraseIdx_of_ge
.
Alias of List.insertIdx_eraseIdx_of_ge
.
Alias of List.insertIdx_eraseIdx_of_le
.
Alias of List.insertIdx_eraseIdx_of_le
.
Alias of List.insertIdx_comm
.
Alias of List.mem_insertIdx
.
Alias of List.insertIdx_of_length_lt
.
Alias of List.insertIdx_length_self
.
Alias of List.length_le_length_insertIdx
.
Alias of List.length_insertIdx_le_succ
.
Alias of List.getElem_insertIdx_of_lt
.
Alias of List.get_insertIdx_of_lt
.
Alias of List.getElem_insertIdx_self
.
Alias of List.get_insertIdx_self
.
Alias of List.getElem_insertIdx_add_succ
.
Alias of List.get_insertIdx_add_succ
.
Alias of List.insertIdx_injective
.