∀ (s : String) (pos : s.Pos) (r : String),
  String.mangleAux✝ s pos r =
    if h : pos = s.endPos then r
    else
      have c := pos.get h;
      have pos := pos.next h;
      if (c.isAlpha || c.isDigit) = true then String.mangleAux✝ s pos (r.push c)
      else
        if c = '_' then String.mangleAux✝ s pos (r ++ "__")
        else
          if c.toNat < 256 then String.mangleAux✝ s pos (String.pushHex✝ 2 c.val (r ++ "_x"))
          else
            if c.toNat < 65536 then String.mangleAux✝ s pos (String.pushHex✝ 4 c.val (r ++ "_u"))
            else String.mangleAux✝ s pos (String.pushHex✝ 8 c.val (r ++ "_U"))