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.

Estimated changes