Delete minus1Trunc.v, close #434

When we start doing some set-math we will likely want a notation for `hexists` and `hor`.