Verifying sequence contents are sequential

Question

I ran into this situation where I suspected that triggers were a problem but I don't quite understand why the triggers are a problem.

The following does not verify.

predicate isSlice(ss: string, s: string, i: int, k: int)
    requires 0 <= i <=k <= |s|
{
    ss == s[i..k]
}

predicate inString(ss: string, s: string, sindex: int, index: int)
    requires index <= |s|
{
    exists i,k :: 0 <= i <=k <= sindex <= index  && isSlice(ss, s, i,k)
}

predicate slicesAreSequential(rs: seq<string>, s: string, index: int) 
    requires index <= |s|
{
    forall i :: 0 <= i < |rs| -1 ==> exists m,n,j,k :: 0 <= m < n <= j < k <= index && isSlice(rs[i], s,m,n) && isSlice(rs[i+1], s, j , k)
}

lemma splitTest(s: string, results: seq<string>)
    requires |results| == |s|
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] in results
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] == results[i]
    requires forall ss: string :: ss in results ==> inString(ss,s, |s|, |s|)
    ensures slicesAreSequential(results, s, |s|)
{
    if |s| > 0 {
        forall i | 0 <= i < |results| -1 
            ensures exists m,n,j,k :: 0 <= m < n <= j < k <= |s| && isSlice(results[i], s,m,n) && isSlice(results[i+1], s, j , k)
        {
            var cur := results[i];
            var next := results[i+1];
            assert isSlice(results[i],s, i,i+1);
            assert isSlice(results[i+1],s, i+1,i+2);
        }
        assert slicesAreSequential(results, s, |s|);
    }else{

    }
}

However, the following version does verify.

predicate slicesAreSequential(rs: seq<string>, s: string, index: int) 
    requires index <= |s|
{
    forall i :: 0 <= i < |rs| -1 ==> bork(rs[i], rs[i+1], s, index)
}

predicate bork(left: string, right: string, s: string, index: int) 
    requires index <= |s|
{
    exists m,n,j,k :: 0 <= m < n <= j < k <= index && isSlice(left, s,m,n) && isSlice(right, s, j , k)
}

lemma splitTest(s: string, results: seq<string>)
    requires |results| == |s|
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] in results
    requires forall i :: 0 <= i < |s| ==> s[i..i+1] == results[i]
    requires forall ss: string :: ss in results ==> inString(ss,s, |s|, |s|)
    ensures slicesAreSequential(results, s, |s|)
{
    if |s| > 0 {
        forall i | 0 <= i < |results| -1 
            ensures exists m,n,j,k :: 0 <= m < n <= j < k <= |s| && isSlice(results[i], s,m,n) && isSlice(results[i+1], s, j , k)
        {
            var cur := results[i];
            var next := results[i+1];
            assert isSlice(results[i],s, i,i+1);
            assert isSlice(results[i+1],s, i+1,i+2);
        }
        assert slicesAreSequential(results, s, |s|);
    }else{

    }
}

Is it because the exists statement does not produce a trigger, even though it is putting some assertion out there?