Delete minus1Trunc.v, close #434

That's much more general than I think is appropriate here; once we have a modality in mind, all the connectives automatically get defined in terms of that: `true` and `and` and `implies` and `forall` are just the fact that the modal types are closed under those operations, while `or` and `exists` and `false` get the modal reflector applied to them.