Prove the assumed lemmas between raw bytes and abstract packets

[jcp19]

• update widen lemma to the current version of absPkt
• prove IO temporary assumptions in path/scion
• prove IO temporary assumptions in router

Should hopefully be done after PRs #243, #248, #261