Merged requested to merge ci/msammler/list into master
These are some lemmas which I need in my development. @robbertkrebbers and I talked about some of them today. I will make another MR with the
rotate function. Let me know what you think and which lemmas seem useful. Also better proofs are always appreciated.