Simpler unwinding

The previous unwinding strategy produced erroneous results in some
cases. This one is much simpler but produces larger formulas. (And
hopefully its correct...)