No problem. I’ve rebased and put the definitions and lemmas in list_monad.v.

@iris-users this should be largely transparent but it turns out there are cases where this breaks downstream code:...

@marijnvanwezel this will need a rebase to resolve the conflicts with !594 (merged). Sorry for that.

That all looks great, thanks!

I made some tweaks, you can find the details in the commit log....

I think I would prefer to handle your MR after this one is done....

Should I rebase !593 on this?