some lemmas about list submseteq

Found in Simuliris, original proofs by @simonspies.

I am not at all sure about the names...

added 1 commit

• c0054b88 - shorten proofs, tweak lemmas (most of it by Robbert)

Compare with previous version

I took care of the other comments.

mentioned in merge request !306 (merged)

added 1 commit

• defb37c6 - make singleton submseteq lemma consistent with Iris

Compare with previous version

resolved all threads

So, good to go?

Modulo nit and CHANGELOG it seems good to me.

resolved all threads

added 1 commit

• 8cb7796f - improve proof

Compare with previous version

added 15 commits

• 8cb7796f...76e9afce - 10 commits from branch master
• d8182e1e - some lemmas about list submseteq
• 88f03cb9 - shorten proofs, tweak lemmas (most of it by Robbert)
• de192271 - make singleton submseteq lemma consistent with Iris
• 5030bc10 - improve proof
• 486ac80b - changelog

Compare with previous version

enabled an automatic merge when the pipeline for 486ac80b succeeds

mentioned in commit cbd68767

merged