Skip to content

Add lemmas `app_cons_eq_inv_{l,r}`.

Robbert Krebbers requested to merge robbert/app_cons_eq_inv_lr into master

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

Merge request reports