Use upd_range instead of word_splice
Use upd_range instead of word_splice

The recursive version is easier to prove.

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