Delete minus1Trunc.v, close #434

I'm against dropping the h, at least unless we replace it with something else.  For `hor` we can steal the infix notation `\/` which looks better anyway; `hexists` is trickier to find a notation for without unicode, but I don't think it's as ugly as `hor` anyway.

My next plan is to implement logic in a generic way over modalities, so that these will become special cases of something like `Oexists` and `Oor`.