Finish proving compose
Finish proving compose

The proof is still incredibly messy (the two cases of destruct out are
still copy-pasted proof scripts), with a lot of automation to be done,
but it's basically true.

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