A quick look at the SSA that prove sees, and my intuition says that prove should indeed be removing both checks. I will look into this more.

Change https://golang.org/cl/273670 mentions this issue: cmd/compile: use list to keep track of slice len/cap in factsTable

The problem is that we only keep 1 slice len/cap SSA value in fact table, so when updating fact table for it, we don't update in all places. In the meantime, you can do:

func f(b []byte, x int, p *uint16) {
	l := len(b)
	switch x {
	case 0:
		if l < 20 {
			return
		}
		*p = binary.BigEndian.Uint16(b[:2])
	case 1:
		if l < 40 {
			return
		}
		*p = binary.BigEndian.Uint16(b[:2])
	}
}

to help compiler proving them.