make it work in general case with non-unitary bit widths. also k-induction doesn't require more than 1 step!
