Removed unnecessary precondition (#403)

Precondition is unnecessary, the file succesfully verifies even without it.

Author: herzamos

verification/utils/slices/slices.gobra

@@ -81,7 +81,6 @@ func Reslice_Bytes(s []byte, start int, end int, p perm) {
 ghost
 requires 0 < p
 requires 0 <= start && start <= end && end <= cap(s)
-requires len(s[start:end]) <= cap(s)
 requires acc(Bytes(s[start:end], 0, len(s[start:end])), p)
 ensures  acc(Bytes(s, start, end), p)
 decreases
@@ -190,4 +189,4 @@ ensures  forall i int :: { &s[subStart:subEnd][i] } 0 <= i && i < len(s[subStart
 decreases
 pure func AssertSliceOverlap(ghost s []byte, ghost subStart int, ghost subEnd int) Unit {
 	return Unit{}
-}
+}