Get closer to proving things about chunkList
Get closer to proving things about chunkList

Need strong induction and a principle that unfolds one level of
chunkList.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl