prove if_ok and almost for_ok
prove if_ok and almost for_ok

except that the for_ok statement is broken w.r.t. final loop iteration
and appears unprovable, so i ended up admit'ing that case..  need to
rethink that "exists lfinal".

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