make it work in general case with non-unitary bit widths. also k-induction doesn't require more than 1 step!
remove superfluous asserts. at least i think they're superfluous, we still need to check with different upstream/downstream widths.
with it
different
ready
