static void web_replaceLabel(WebNode n, S from, S to) {
  if (n == null) ret;
  int i = n.labels.indexOf(n.web.parseLabel(from));
  if (i >= 0)
    n.labels.set(i, nweb.parseLabel(to));
}