Delete minus1Trunc.v, close #434

I guess you're referring to the line `assert (H : forall z w : G, z = w) by apply allpath_hprop;` in the original tactic.  I removed that because I thought it was only necessary because the truncatedness hypothesis of the old `minus1Trunc_rect_nondep` was `forall (z w : B), z = w` rather than `IsHProp B` so that the latter had to be automatically proven from the former.  Now the hypothesis of `Trunc_rect_nondep` is `IsTrunc n X` so that shouldn't be necessary.  But you think it should still be there so that the tactic fails if the goal isn't truncated?