be a bit more explicit in the partition proof
record a draft to make it easier to collaborate