restructure I/IW instantiation files

There are a lot of lemmas inside of [abstract/ideal/iw_instantiation.v] that are not specific to ideal uni-processor. This MR moves such lemmas to [abstract/iw_auxiliary.v]