Fix bug in remove_spec
Do a few proofs in MMapWeakList.v (proving is addictive)