Index Checker `startsWith` refinement

Consider this code (which is in checker/tests/index/StartsEndsWith.java):

  final String prefix;

  String propertyName(String methodName) {
    if (methodName.startsWith(prefix)) {
      String result = methodName.substring(prefix.length());
      return result;
    } else {
      return null;
    }
  }

The Index Checker issues the following warning:

StartsEndsWith.java:17: error: [argument] incompatible argument for parameter beginIndex of substring.
      String result = methodName.substring(prefix.length());
                                                        ^
  found   : @LTEqLengthOf("this.prefix") int
  required: @LTEqLengthOf("methodName") int

but the code is correct because methodName is at least as long as this.prefix.

Reproduce the warning using checker/tests/index/StartsEndsWith.java and read the Index Checker handling involved in startsWith refinement. Determine how the length relationship between methodName and prefix should be represented, then verify that the shown substring call is accepted without weakening valid index checks.