Theorem List.length_eraseIdx_add_one

Modification history