Renamed `app_cons_eq_inv_{l,r}`, and added derived versions for `prefix/suffix`

Renamed the lemmas app_cons_eq_inv_{l,r}, to elem_of_app_cons_inv_{l,r}, to be more descriptive and consistent with existing lemmas.

Additionally, derived versions for prefix/suffix, as they recall some non-immediate properties of the relations on similar list structures.

mentioned in merge request !363 (merged)

added 1 commit

• 2a3b29da - Made proof of [prefix_app_inv] in line with that of [suffix_app_inv]

Compare with previous version

Can you rebase, add the lemma for postfix, and put them in the same style as the ones in !363 (merged).

added 28 commits

• 2a3b29da...f71300ea - 26 commits from branch iris:master
• fb27a857 - Added useful lemmas for [prefix]
• 22e7199d - Made proof of [prefix_app_inv] in line with that of [suffix_app_inv]

Compare with previous version

added 1 commit

• 844a0f13 - Added suffix variant, renamed lemmas, proved in terms of existing

Compare with previous version

resolved all threads

Can you also update the title + description of this MR?

added 1 commit

• 8d2492d9 - Improved proofs and changed names of lemmas

Compare with previous version

resolved all threads

changed title from Added useful lemmas for [prefix] to Added {+derived versions of app_cons_eq_inv_{l,r}+} for {++}prefix{+/suffix+}

changed the description

resolved all threads

added 1 commit

• c8a409d8 - Changed names of new lemmas

Compare with previous version

added 1 commit

• 2b4f0c78 - Changed names of lemmas again

Compare with previous version

resolved all threads

added 1 commit

• b5208154 - Another lemma name change

Compare with previous version

resolved all threads

added 1 commit

• 346342ba - Another name change - Also for dependent lemmas

Compare with previous version

LGTM. Can you update the MR title and add a proper description in the text (including documenting the recent renames)?

changed title from {-Added derived versions of app_cons_eq_inv_{l,r}-} for prefix/suffix to {+Renamed app_cons_eq_inv_{l,r}, and added derived versions+} for prefix/suffix

changed the description

@iris-users This MR is a breaking change if you already rely on the lemmas from !363 (merged) (merged 5 days ago).

merged

mentioned in commit 907a40ef

Thanks @jihgfee for the fixes! Merged.