static String dropPrefixMandatory(String prefix, String s) {
  if (s.startsWith(prefix))
    return s.substring(prefix.length());
  else
    throw fail("Prefix " + prefix + " not found in: " + s);
}