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]
assigned to @bbb
added 1 commit
Compare with previous version
resolved all threads
added 3 commits
@bbb, should be ready
