Some fixes and progress in icombine_app proof
Some fixes and progress in icombine_app proof

Structure should mirror combine_app from Rec, but that doesn't seem to
work due to more eq_rects in the way.

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