Sketch out proof of bf_shrink_ok
Sketch out proof of bf_shrink_ok

Mirroring the bf_expand_ok proof, but with its own rep lemma for
shrinking the file.

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