Move implications of rep function up
Move implications of rep function up

All lemmas that basically follow from (parts of) [array_item_file f
ilist]. These are useful throughout and I often need one at some
earlier proof.

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