Optimize `DIP n {}`

This MR adds an optimization rule to transform DIP n {}; i into i and prove the correctness of this optimization rule.