I just took a preliminary peek, @josharian I think this may relate to #25086. Information from a non-control op (Phi) in a non-branching block is required to complete the inference from i back to len(x) and len(y).

This code:

n := len(x)
if len(y) < n {
	n = len(y)
}

concludes with a Plain SSA block containing just a Phi Op

b2: ← b3 b4
    v47 = Phi <int> v9 v8 (n[int])
Plain → b5

where v8/v9 are len(x)/len(y). This block doesn't branch, so prove doesn't use it. Without the relationship between v47 and len(x)/len(y), the inferential chain from i back to len(x) and len(y) is broken.

v8 = SliceLen <int> v6 (n[int])
v9 = SliceLen <int> v7
...
v47 = Phi <int> v9 v8 (n[int])
...
v16 = Less64 <bool> v14 v47
...
    v20 = IsInBounds <bool> v14 v8
...
    v30 = IsInBounds <bool> v14 v9