Post #1816217

@dwarn I was wondering whether your setting might be different, and whether that actually matters. I think there might be quite a low-level proof that should work always. I wanted to formalise some of these statements myself. Maybe a project for the summer.