Commit 2024-05-05 22:56 07e4145a
View on Github →chore: shorten proof of List.sizeOf_dropSlice_lt (#12678)
Replaces an induction
with direct usage of drop_sizeOf_le
.
This simplification was found by tryAtEachStep.
chore: shorten proof of List.sizeOf_dropSlice_lt (#12678)
Replaces an induction
with direct usage of drop_sizeOf_le
.
This simplification was found by tryAtEachStep.