An error occurred while fetching the assigned milestone of the selected merge_request.
This MR contains two commits: One with the actual lemmas, and one to perform some rearrangements. To prove the _r
variant, I needed properties of reverse
. I thus moved the reverse
lemmas above the elem_of
lemmas.
The lemmas in this MR generalize the ones in !356 (merged). They also allow proving a variant for suffix_of
, which is missing in that MR.
/cc @jihgfee