Delete minus1Trunc.v, close #434

You removed the check that the goal is truncated, though; I believe we'll now be left with a goal of proving that it is truncated if typeclass resolution fails, where before the `assert ... by` would fail.