Add lemmas `app_cons_eq_inv_{l,r}`.

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

mentioned in merge request !356 (merged)

These lemmas seem useful. As discussed elsewhere, a direct consequence of their conclusion is that x = y and l2 = k2 (for the prefix variant). Even though these are immediate (from something like simplify_eq), I think it is nicer to add them. Especially since the referenced variants would instead have x = y and l2 prefix_of k2, which is not as trivial.

added 1 commit

• 59468247 - Add lemmas `app_cons_eq_inv_{l,r}`.

Compare with previous version

Thank you @jihgfee. I have added all the equalities as additional conclusions.

Awesome. LGTM!

Merging. Thanks.

merged

mentioned in commit f71300ea