diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index 0ec4876f2d..fbb386b5fe 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -1,266 +1,266 @@
 byte_rect =
-fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
-  (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
-  (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") 
-  (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") 
-  (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) =>
+fun (P : byte -> Type) (x00 : P "000") (x01 : P "001") (x02 : P "002") (x03 : P "003") (x04 : P "004") (x05 : P "005") (x06 : P "006") (x07 : P "007") (x08 : P "008") (x09 : P "009") (x0a : P "010") (x0b : P "011") (x0c : P "012") (x0d : P "013") (x0e : P "014") (x0f : P "015") (x10 : P "016") (x11 : P "017") (x12 : P "018") (x13 : P "019") (x14 : P "020") (x15 : P "021") (x16 : P "022") (x17 : P "023") (x18 : P "024") (x19 : P "025") (x1a : P "026") (x1b : P "027") (x1c : P "028") (x1d : P "029") (x1e : P "030") (x1f : P "031") (x20 : P " ") (x21 : P "!") (x22 : P """") (x23 : P "#") (x24 : P "$") (x25 : P "%") (x26 : P "&") (x27 : P "'") (x28 : P "(") (x29 : P ")") (x2a : P "*") (x2b : P "+") (x2c : P ",") (x2d : P "-") (x2e : P ".") (x2f : P "/") (x30 : P "0") (x31 : P "1") (x32 : P "2") (x33 : P "3") (x34 : P "4") (x35 : P "5") (x36 : P "6") (x37 : P "7") (x38 : P "8") (x39 : P "9") (x3a : P ":") (x3b : P ";") (x3c : P "<") (x3d : P "=") (x3e : P ">") (x3f : P "?") 
+  (x40 : P "@") (x41 : P "A") (x42 : P "B") (x43 : P "C") (x44 : P "D") (x45 : P "E") (x46 : P "F") (x47 : P "G") (x48 : P "H") (x49 : P "I") (x4a : P "J") (x4b : P "K") (x4c : P "L") (x4d : P "M") (x4e : P "N") (x4f : P "O") (x50 : P "P") (x51 : P "Q") (x52 : P "R") (x53 : P "S") (x54 : P "T") (x55 : P "U") (x56 : P "V") (x57 : P "W") (x58 : P "X") (x59 : P "Y") (x5a : P "Z") (x5b : P "[") (x5c : P "\") (x5d : P "]") (x5e : P "^") (x5f : P "_") (x60 : P "`") (x61 : P "a") (x62 : P "b") (x63 : P "c") (x64 : P "d") (x65 : P "e") (x66 : P "f") (x67 : P "g") (x68 : P "h") (x69 : P "i") (x6a : P "j") (x6b : P "k") (x6c : P "l") (x6d : P "m") (x6e : P "n") (x6f : P "o") (x70 : P "p") (x71 : P "q") (x72 : P "r") (x73 : P "s") (x74 : P "t") (x75 : P "u") (x76 : P "v") (x77 : P "w") (x78 : P "x") (x79 : P "y") (x7a : P "z") (x7b : P "{") (x7c : P "|") (x7d : P "}") (x7e : P "~") (x7f : P "127") (x80 : P "128") (x81 : P "129") (x82 : P "130") (x83 : P "131") (x84 : P "132") 
+  (x85 : P "133") (x86 : P "134") (x87 : P "135") (x88 : P "136") (x89 : P "137") (x8a : P "138") (x8b : P "139") (x8c : P "140") (x8d : P "141") (x8e : P "142") (x8f : P "143") (x90 : P "144") (x91 : P "145") (x92 : P "146") (x93 : P "147") (x94 : P "148") (x95 : P "149") (x96 : P "150") (x97 : P "151") (x98 : P "152") (x99 : P "153") (x9a : P "154") (x9b : P "155") (x9c : P "156") (x9d : P "157") (x9e : P "158") (x9f : P "159") (xa0 : P "160") (xa1 : P "161") (xa2 : P "162") (xa3 : P "163") (xa4 : P "164") (xa5 : P "165") (xa6 : P "166") (xa7 : P "167") (xa8 : P "168") (xa9 : P "169") (xaa : P "170") (xab : P "171") (xac : P "172") (xad : P "173") (xae : P "174") (xaf : P "175") (xb0 : P "176") (xb1 : P "177") (xb2 : P "178") (xb3 : P "179") (xb4 : P "180") (xb5 : P "181") (xb6 : P "182") (xb7 : P "183") (xb8 : P "184") (xb9 : P "185") (xba : P "186") (xbb : P "187") (xbc : P "188") (xbd : P "189") (xbe : P "190") (xbf : P "191") (xc0 : P "192") (xc1 : P "193") 
+  (xc2 : P "194") (xc3 : P "195") (xc4 : P "196") (xc5 : P "197") (xc6 : P "198") (xc7 : P "199") (xc8 : P "200") (xc9 : P "201") (xca : P "202") (xcb : P "203") (xcc : P "204") (xcd : P "205") (xce : P "206") (xcf : P "207") (xd0 : P "208") (xd1 : P "209") (xd2 : P "210") (xd3 : P "211") (xd4 : P "212") (xd5 : P "213") (xd6 : P "214") (xd7 : P "215") (xd8 : P "216") (xd9 : P "217") (xda : P "218") (xdb : P "219") (xdc : P "220") (xdd : P "221") (xde : P "222") (xdf : P "223") (xe0 : P "224") (xe1 : P "225") (xe2 : P "226") (xe3 : P "227") (xe4 : P "228") (xe5 : P "229") (xe6 : P "230") (xe7 : P "231") (xe8 : P "232") (xe9 : P "233") (xea : P "234") (xeb : P "235") (xec : P "236") (xed : P "237") (xee : P "238") (xef : P "239") (xf0 : P "240") (xf1 : P "241") (xf2 : P "242") (xf3 : P "243") (xf4 : P "244") (xf5 : P "245") (xf6 : P "246") (xf7 : P "247") (xf8 : P "248") (xf9 : P "249") (xfa : P "250") (xfb : P "251") (xfc : P "252") (xfd : P "253") (xfe : P "254") 
+  (xff : P "255") (b : byte) =>
 match b as b0 return (P b0) with
-| "000" => f
-| "001" => f0
-| "002" => f1
-| "003" => f2
-| "004" => f3
-| "005" => f4
-| "006" => f5
-| "007" => f6
-| "008" => f7
-| "009" => f8
-| "010" => f9
-| "011" => f10
-| "012" => f11
-| "013" => f12
-| "014" => f13
-| "015" => f14
-| "016" => f15
-| "017" => f16
-| "018" => f17
-| "019" => f18
-| "020" => f19
-| "021" => f20
-| "022" => f21
-| "023" => f22
-| "024" => f23
-| "025" => f24
-| "026" => f25
-| "027" => f26
-| "028" => f27
-| "029" => f28
-| "030" => f29
-| "031" => f30
-| " " => f31
-| "!" => f32
-| """" => f33
-| "#" => f34
-| "$" => f35
-| "%" => f36
-| "&" => f37
-| "'" => f38
-| "(" => f39
-| ")" => f40
-| "*" => f41
-| "+" => f42
-| "," => f43
-| "-" => f44
-| "." => f45
-| "/" => f46
-| "0" => f47
-| "1" => f48
-| "2" => f49
-| "3" => f50
-| "4" => f51
-| "5" => f52
-| "6" => f53
-| "7" => f54
-| "8" => f55
-| "9" => f56
-| ":" => f57
-| ";" => f58
-| "<" => f59
-| "=" => f60
-| ">" => f61
-| "?" => f62
-| "@" => f63
-| "A" => f64
-| "B" => f65
-| "C" => f66
-| "D" => f67
-| "E" => f68
-| "F" => f69
-| "G" => f70
-| "H" => f71
-| "I" => f72
-| "J" => f73
-| "K" => f74
-| "L" => f75
-| "M" => f76
-| "N" => f77
-| "O" => f78
-| "P" => f79
-| "Q" => f80
-| "R" => f81
-| "S" => f82
-| "T" => f83
-| "U" => f84
-| "V" => f85
-| "W" => f86
-| "X" => f87
-| "Y" => f88
-| "Z" => f89
-| "[" => f90
-| "\" => f91
-| "]" => f92
-| "^" => f93
-| "_" => f94
-| "`" => f95
-| "a" => f96
-| "b" => f97
-| "c" => f98
-| "d" => f99
-| "e" => f100
-| "f" => f101
-| "g" => f102
-| "h" => f103
-| "i" => f104
-| "j" => f105
-| "k" => f106
-| "l" => f107
-| "m" => f108
-| "n" => f109
-| "o" => f110
-| "p" => f111
-| "q" => f112
-| "r" => f113
-| "s" => f114
-| "t" => f115
-| "u" => f116
-| "v" => f117
-| "w" => f118
-| "x" => f119
-| "y" => f120
-| "z" => f121
-| "{" => f122
-| "|" => f123
-| "}" => f124
-| "~" => f125
-| "127" => f126
-| "128" => f127
-| "129" => f128
-| "130" => f129
-| "131" => f130
-| "132" => f131
-| "133" => f132
-| "134" => f133
-| "135" => f134
-| "136" => f135
-| "137" => f136
-| "138" => f137
-| "139" => f138
-| "140" => f139
-| "141" => f140
-| "142" => f141
-| "143" => f142
-| "144" => f143
-| "145" => f144
-| "146" => f145
-| "147" => f146
-| "148" => f147
-| "149" => f148
-| "150" => f149
-| "151" => f150
-| "152" => f151
-| "153" => f152
-| "154" => f153
-| "155" => f154
-| "156" => f155
-| "157" => f156
-| "158" => f157
-| "159" => f158
-| "160" => f159
-| "161" => f160
-| "162" => f161
-| "163" => f162
-| "164" => f163
-| "165" => f164
-| "166" => f165
-| "167" => f166
-| "168" => f167
-| "169" => f168
-| "170" => f169
-| "171" => f170
-| "172" => f171
-| "173" => f172
-| "174" => f173
-| "175" => f174
-| "176" => f175
-| "177" => f176
-| "178" => f177
-| "179" => f178
-| "180" => f179
-| "181" => f180
-| "182" => f181
-| "183" => f182
-| "184" => f183
-| "185" => f184
-| "186" => f185
-| "187" => f186
-| "188" => f187
-| "189" => f188
-| "190" => f189
-| "191" => f190
-| "192" => f191
-| "193" => f192
-| "194" => f193
-| "195" => f194
-| "196" => f195
-| "197" => f196
-| "198" => f197
-| "199" => f198
-| "200" => f199
-| "201" => f200
-| "202" => f201
-| "203" => f202
-| "204" => f203
-| "205" => f204
-| "206" => f205
-| "207" => f206
-| "208" => f207
-| "209" => f208
-| "210" => f209
-| "211" => f210
-| "212" => f211
-| "213" => f212
-| "214" => f213
-| "215" => f214
-| "216" => f215
-| "217" => f216
-| "218" => f217
-| "219" => f218
-| "220" => f219
-| "221" => f220
-| "222" => f221
-| "223" => f222
-| "224" => f223
-| "225" => f224
-| "226" => f225
-| "227" => f226
-| "228" => f227
-| "229" => f228
-| "230" => f229
-| "231" => f230
-| "232" => f231
-| "233" => f232
-| "234" => f233
-| "235" => f234
-| "236" => f235
-| "237" => f236
-| "238" => f237
-| "239" => f238
-| "240" => f239
-| "241" => f240
-| "242" => f241
-| "243" => f242
-| "244" => f243
-| "245" => f244
-| "246" => f245
-| "247" => f246
-| "248" => f247
-| "249" => f248
-| "250" => f249
-| "251" => f250
-| "252" => f251
-| "253" => f252
-| "254" => f253
-| "255" => f254
+| "000" => x00
+| "001" => x01
+| "002" => x02
+| "003" => x03
+| "004" => x04
+| "005" => x05
+| "006" => x06
+| "007" => x07
+| "008" => x08
+| "009" => x09
+| "010" => x0a
+| "011" => x0b
+| "012" => x0c
+| "013" => x0d
+| "014" => x0e
+| "015" => x0f
+| "016" => x10
+| "017" => x11
+| "018" => x12
+| "019" => x13
+| "020" => x14
+| "021" => x15
+| "022" => x16
+| "023" => x17
+| "024" => x18
+| "025" => x19
+| "026" => x1a
+| "027" => x1b
+| "028" => x1c
+| "029" => x1d
+| "030" => x1e
+| "031" => x1f
+| " " => x20
+| "!" => x21
+| """" => x22
+| "#" => x23
+| "$" => x24
+| "%" => x25
+| "&" => x26
+| "'" => x27
+| "(" => x28
+| ")" => x29
+| "*" => x2a
+| "+" => x2b
+| "," => x2c
+| "-" => x2d
+| "." => x2e
+| "/" => x2f
+| "0" => x30
+| "1" => x31
+| "2" => x32
+| "3" => x33
+| "4" => x34
+| "5" => x35
+| "6" => x36
+| "7" => x37
+| "8" => x38
+| "9" => x39
+| ":" => x3a
+| ";" => x3b
+| "<" => x3c
+| "=" => x3d
+| ">" => x3e
+| "?" => x3f
+| "@" => x40
+| "A" => x41
+| "B" => x42
+| "C" => x43
+| "D" => x44
+| "E" => x45
+| "F" => x46
+| "G" => x47
+| "H" => x48
+| "I" => x49
+| "J" => x4a
+| "K" => x4b
+| "L" => x4c
+| "M" => x4d
+| "N" => x4e
+| "O" => x4f
+| "P" => x50
+| "Q" => x51
+| "R" => x52
+| "S" => x53
+| "T" => x54
+| "U" => x55
+| "V" => x56
+| "W" => x57
+| "X" => x58
+| "Y" => x59
+| "Z" => x5a
+| "[" => x5b
+| "\" => x5c
+| "]" => x5d
+| "^" => x5e
+| "_" => x5f
+| "`" => x60
+| "a" => x61
+| "b" => x62
+| "c" => x63
+| "d" => x64
+| "e" => x65
+| "f" => x66
+| "g" => x67
+| "h" => x68
+| "i" => x69
+| "j" => x6a
+| "k" => x6b
+| "l" => x6c
+| "m" => x6d
+| "n" => x6e
+| "o" => x6f
+| "p" => x70
+| "q" => x71
+| "r" => x72
+| "s" => x73
+| "t" => x74
+| "u" => x75
+| "v" => x76
+| "w" => x77
+| "x" => x78
+| "y" => x79
+| "z" => x7a
+| "{" => x7b
+| "|" => x7c
+| "}" => x7d
+| "~" => x7e
+| "127" => x7f
+| "128" => x80
+| "129" => x81
+| "130" => x82
+| "131" => x83
+| "132" => x84
+| "133" => x85
+| "134" => x86
+| "135" => x87
+| "136" => x88
+| "137" => x89
+| "138" => x8a
+| "139" => x8b
+| "140" => x8c
+| "141" => x8d
+| "142" => x8e
+| "143" => x8f
+| "144" => x90
+| "145" => x91
+| "146" => x92
+| "147" => x93
+| "148" => x94
+| "149" => x95
+| "150" => x96
+| "151" => x97
+| "152" => x98
+| "153" => x99
+| "154" => x9a
+| "155" => x9b
+| "156" => x9c
+| "157" => x9d
+| "158" => x9e
+| "159" => x9f
+| "160" => xa0
+| "161" => xa1
+| "162" => xa2
+| "163" => xa3
+| "164" => xa4
+| "165" => xa5
+| "166" => xa6
+| "167" => xa7
+| "168" => xa8
+| "169" => xa9
+| "170" => xaa
+| "171" => xab
+| "172" => xac
+| "173" => xad
+| "174" => xae
+| "175" => xaf
+| "176" => xb0
+| "177" => xb1
+| "178" => xb2
+| "179" => xb3
+| "180" => xb4
+| "181" => xb5
+| "182" => xb6
+| "183" => xb7
+| "184" => xb8
+| "185" => xb9
+| "186" => xba
+| "187" => xbb
+| "188" => xbc
+| "189" => xbd
+| "190" => xbe
+| "191" => xbf
+| "192" => xc0
+| "193" => xc1
+| "194" => xc2
+| "195" => xc3
+| "196" => xc4
+| "197" => xc5
+| "198" => xc6
+| "199" => xc7
+| "200" => xc8
+| "201" => xc9
+| "202" => xca
+| "203" => xcb
+| "204" => xcc
+| "205" => xcd
+| "206" => xce
+| "207" => xcf
+| "208" => xd0
+| "209" => xd1
+| "210" => xd2
+| "211" => xd3
+| "212" => xd4
+| "213" => xd5
+| "214" => xd6
+| "215" => xd7
+| "216" => xd8
+| "217" => xd9
+| "218" => xda
+| "219" => xdb
+| "220" => xdc
+| "221" => xdd
+| "222" => xde
+| "223" => xdf
+| "224" => xe0
+| "225" => xe1
+| "226" => xe2
+| "227" => xe3
+| "228" => xe4
+| "229" => xe5
+| "230" => xe6
+| "231" => xe7
+| "232" => xe8
+| "233" => xe9
+| "234" => xea
+| "235" => xeb
+| "236" => xec
+| "237" => xed
+| "238" => xee
+| "239" => xef
+| "240" => xf0
+| "241" => xf1
+| "242" => xf2
+| "243" => xf3
+| "244" => xf4
+| "245" => xf5
+| "246" => xf6
+| "247" => xf7
+| "248" => xf8
+| "249" => xf9
+| "250" => xfa
+| "251" => xfb
+| "252" => xfc
+| "253" => xfd
+| "254" => xfe
+| "255" => xff
 end
      : forall P : byte -> Type,
        P "000" ->
@@ -433,8 +433,8 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Arguments byte_rect P%_function_scope f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 
-  f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 b%_byte_scope
+Arguments byte_rect P%_function_scope x00 x01 x02 x03 x04 x05 x06 x07 x08 x09 x0a x0b x0c x0d x0e x0f x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x1a x1b x1c x1d x1e x1f x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x2a x2b x2c x2d x2e x2f x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x3a x3b x3c x3d x3e x3f x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x4a x4b x4c x4d x4e x4f x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x5a x5b x5c x5d x5e x5f x60 x61 x62 x63 x64 x65 x66 x67 x68 x69 x6a x6b x6c x6d x6e x6f x70 x71 x72 x73 x74 x75 x76 x77 x78 x79 x7a x7b x7c x7d x7e x7f x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x8a x8b x8c x8d x8e x8f x90 x91 x92 x93 x94 x95 x96 x97 x98 x99 x9a x9b x9c x9d x9e x9f xa0 xa1 xa2 xa3 xa4 xa5 xa6 xa7 xa8 xa9 xaa xab xac xad xae xaf xb0 xb1 xb2 xb3 xb4 xb5 xb6 xb7 xb8 xb9 xba xbb xbc xbd xbe xbf xc0 xc1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 xca xcb xcc xcd xce xcf xd0 xd1 xd2 xd3 xd4 xd5 xd6 xd7 xd8 xd9 xda xdb xdc xdd xde xdf xe0 xe1 xe2 xe3 xe4 xe5 xe6 xe7 xe8 xe9 
+  xea xeb xec xed xee xef xf0 xf1 xf2 xf3 xf4 xf5 xf6 xf7 xf8 xf9 xfa xfb xfc xfd xfe xff b%_byte_scope
 byte_rec =
 fun P : byte -> Set => byte_rect P
      : forall P : byte -> Set,
@@ -608,271 +608,271 @@ fun P : byte -> Set => byte_rect P
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Arguments byte_rec P%_function_scope f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 
-  f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 b%_byte_scope
+Arguments byte_rec P%_function_scope x00 x01 x02 x03 x04 x05 x06 x07 x08 x09 x0a x0b x0c x0d x0e x0f x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x1a x1b x1c x1d x1e x1f x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x2a x2b x2c x2d x2e x2f x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x3a x3b x3c x3d x3e x3f x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x4a x4b x4c x4d x4e x4f x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x5a x5b x5c x5d x5e x5f x60 x61 x62 x63 x64 x65 x66 x67 x68 x69 x6a x6b x6c x6d x6e x6f x70 x71 x72 x73 x74 x75 x76 x77 x78 x79 x7a x7b x7c x7d x7e x7f x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x8a x8b x8c x8d x8e x8f x90 x91 x92 x93 x94 x95 x96 x97 x98 x99 x9a x9b x9c x9d x9e x9f xa0 xa1 xa2 xa3 xa4 xa5 xa6 xa7 xa8 xa9 xaa xab xac xad xae xaf xb0 xb1 xb2 xb3 xb4 xb5 xb6 xb7 xb8 xb9 xba xbb xbc xbd xbe xbf xc0 xc1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 xca xcb xcc xcd xce xcf xd0 xd1 xd2 xd3 xd4 xd5 xd6 xd7 xd8 xd9 xda xdb xdc xdd xde xdf xe0 xe1 xe2 xe3 xe4 xe5 xe6 xe7 xe8 xe9 
+  xea xeb xec xed xee xef xf0 xf1 xf2 xf3 xf4 xf5 xf6 xf7 xf8 xf9 xfa xfb xfc xfd xfe xff b%_byte_scope
 byte_ind =
-fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
-  (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
-  (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") 
-  (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") 
-  (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) =>
+fun (P : byte -> Prop) (x00 : P "000") (x01 : P "001") (x02 : P "002") (x03 : P "003") (x04 : P "004") (x05 : P "005") (x06 : P "006") (x07 : P "007") (x08 : P "008") (x09 : P "009") (x0a : P "010") (x0b : P "011") (x0c : P "012") (x0d : P "013") (x0e : P "014") (x0f : P "015") (x10 : P "016") (x11 : P "017") (x12 : P "018") (x13 : P "019") (x14 : P "020") (x15 : P "021") (x16 : P "022") (x17 : P "023") (x18 : P "024") (x19 : P "025") (x1a : P "026") (x1b : P "027") (x1c : P "028") (x1d : P "029") (x1e : P "030") (x1f : P "031") (x20 : P " ") (x21 : P "!") (x22 : P """") (x23 : P "#") (x24 : P "$") (x25 : P "%") (x26 : P "&") (x27 : P "'") (x28 : P "(") (x29 : P ")") (x2a : P "*") (x2b : P "+") (x2c : P ",") (x2d : P "-") (x2e : P ".") (x2f : P "/") (x30 : P "0") (x31 : P "1") (x32 : P "2") (x33 : P "3") (x34 : P "4") (x35 : P "5") (x36 : P "6") (x37 : P "7") (x38 : P "8") (x39 : P "9") (x3a : P ":") (x3b : P ";") (x3c : P "<") (x3d : P "=") (x3e : P ">") (x3f : P "?") 
+  (x40 : P "@") (x41 : P "A") (x42 : P "B") (x43 : P "C") (x44 : P "D") (x45 : P "E") (x46 : P "F") (x47 : P "G") (x48 : P "H") (x49 : P "I") (x4a : P "J") (x4b : P "K") (x4c : P "L") (x4d : P "M") (x4e : P "N") (x4f : P "O") (x50 : P "P") (x51 : P "Q") (x52 : P "R") (x53 : P "S") (x54 : P "T") (x55 : P "U") (x56 : P "V") (x57 : P "W") (x58 : P "X") (x59 : P "Y") (x5a : P "Z") (x5b : P "[") (x5c : P "\") (x5d : P "]") (x5e : P "^") (x5f : P "_") (x60 : P "`") (x61 : P "a") (x62 : P "b") (x63 : P "c") (x64 : P "d") (x65 : P "e") (x66 : P "f") (x67 : P "g") (x68 : P "h") (x69 : P "i") (x6a : P "j") (x6b : P "k") (x6c : P "l") (x6d : P "m") (x6e : P "n") (x6f : P "o") (x70 : P "p") (x71 : P "q") (x72 : P "r") (x73 : P "s") (x74 : P "t") (x75 : P "u") (x76 : P "v") (x77 : P "w") (x78 : P "x") (x79 : P "y") (x7a : P "z") (x7b : P "{") (x7c : P "|") (x7d : P "}") (x7e : P "~") (x7f : P "127") (x80 : P "128") (x81 : P "129") (x82 : P "130") (x83 : P "131") (x84 : P "132") 
+  (x85 : P "133") (x86 : P "134") (x87 : P "135") (x88 : P "136") (x89 : P "137") (x8a : P "138") (x8b : P "139") (x8c : P "140") (x8d : P "141") (x8e : P "142") (x8f : P "143") (x90 : P "144") (x91 : P "145") (x92 : P "146") (x93 : P "147") (x94 : P "148") (x95 : P "149") (x96 : P "150") (x97 : P "151") (x98 : P "152") (x99 : P "153") (x9a : P "154") (x9b : P "155") (x9c : P "156") (x9d : P "157") (x9e : P "158") (x9f : P "159") (xa0 : P "160") (xa1 : P "161") (xa2 : P "162") (xa3 : P "163") (xa4 : P "164") (xa5 : P "165") (xa6 : P "166") (xa7 : P "167") (xa8 : P "168") (xa9 : P "169") (xaa : P "170") (xab : P "171") (xac : P "172") (xad : P "173") (xae : P "174") (xaf : P "175") (xb0 : P "176") (xb1 : P "177") (xb2 : P "178") (xb3 : P "179") (xb4 : P "180") (xb5 : P "181") (xb6 : P "182") (xb7 : P "183") (xb8 : P "184") (xb9 : P "185") (xba : P "186") (xbb : P "187") (xbc : P "188") (xbd : P "189") (xbe : P "190") (xbf : P "191") (xc0 : P "192") (xc1 : P "193") 
+  (xc2 : P "194") (xc3 : P "195") (xc4 : P "196") (xc5 : P "197") (xc6 : P "198") (xc7 : P "199") (xc8 : P "200") (xc9 : P "201") (xca : P "202") (xcb : P "203") (xcc : P "204") (xcd : P "205") (xce : P "206") (xcf : P "207") (xd0 : P "208") (xd1 : P "209") (xd2 : P "210") (xd3 : P "211") (xd4 : P "212") (xd5 : P "213") (xd6 : P "214") (xd7 : P "215") (xd8 : P "216") (xd9 : P "217") (xda : P "218") (xdb : P "219") (xdc : P "220") (xdd : P "221") (xde : P "222") (xdf : P "223") (xe0 : P "224") (xe1 : P "225") (xe2 : P "226") (xe3 : P "227") (xe4 : P "228") (xe5 : P "229") (xe6 : P "230") (xe7 : P "231") (xe8 : P "232") (xe9 : P "233") (xea : P "234") (xeb : P "235") (xec : P "236") (xed : P "237") (xee : P "238") (xef : P "239") (xf0 : P "240") (xf1 : P "241") (xf2 : P "242") (xf3 : P "243") (xf4 : P "244") (xf5 : P "245") (xf6 : P "246") (xf7 : P "247") (xf8 : P "248") (xf9 : P "249") (xfa : P "250") (xfb : P "251") (xfc : P "252") (xfd : P "253") (xfe : P "254") 
+  (xff : P "255") (b : byte) =>
 match b as b0 return (P b0) with
-| "000" => f
-| "001" => f0
-| "002" => f1
-| "003" => f2
-| "004" => f3
-| "005" => f4
-| "006" => f5
-| "007" => f6
-| "008" => f7
-| "009" => f8
-| "010" => f9
-| "011" => f10
-| "012" => f11
-| "013" => f12
-| "014" => f13
-| "015" => f14
-| "016" => f15
-| "017" => f16
-| "018" => f17
-| "019" => f18
-| "020" => f19
-| "021" => f20
-| "022" => f21
-| "023" => f22
-| "024" => f23
-| "025" => f24
-| "026" => f25
-| "027" => f26
-| "028" => f27
-| "029" => f28
-| "030" => f29
-| "031" => f30
-| " " => f31
-| "!" => f32
-| """" => f33
-| "#" => f34
-| "$" => f35
-| "%" => f36
-| "&" => f37
-| "'" => f38
-| "(" => f39
-| ")" => f40
-| "*" => f41
-| "+" => f42
-| "," => f43
-| "-" => f44
-| "." => f45
-| "/" => f46
-| "0" => f47
-| "1" => f48
-| "2" => f49
-| "3" => f50
-| "4" => f51
-| "5" => f52
-| "6" => f53
-| "7" => f54
-| "8" => f55
-| "9" => f56
-| ":" => f57
-| ";" => f58
-| "<" => f59
-| "=" => f60
-| ">" => f61
-| "?" => f62
-| "@" => f63
-| "A" => f64
-| "B" => f65
-| "C" => f66
-| "D" => f67
-| "E" => f68
-| "F" => f69
-| "G" => f70
-| "H" => f71
-| "I" => f72
-| "J" => f73
-| "K" => f74
-| "L" => f75
-| "M" => f76
-| "N" => f77
-| "O" => f78
-| "P" => f79
-| "Q" => f80
-| "R" => f81
-| "S" => f82
-| "T" => f83
-| "U" => f84
-| "V" => f85
-| "W" => f86
-| "X" => f87
-| "Y" => f88
-| "Z" => f89
-| "[" => f90
-| "\" => f91
-| "]" => f92
-| "^" => f93
-| "_" => f94
-| "`" => f95
-| "a" => f96
-| "b" => f97
-| "c" => f98
-| "d" => f99
-| "e" => f100
-| "f" => f101
-| "g" => f102
-| "h" => f103
-| "i" => f104
-| "j" => f105
-| "k" => f106
-| "l" => f107
-| "m" => f108
-| "n" => f109
-| "o" => f110
-| "p" => f111
-| "q" => f112
-| "r" => f113
-| "s" => f114
-| "t" => f115
-| "u" => f116
-| "v" => f117
-| "w" => f118
-| "x" => f119
-| "y" => f120
-| "z" => f121
-| "{" => f122
-| "|" => f123
-| "}" => f124
-| "~" => f125
-| "127" => f126
-| "128" => f127
-| "129" => f128
-| "130" => f129
-| "131" => f130
-| "132" => f131
-| "133" => f132
-| "134" => f133
-| "135" => f134
-| "136" => f135
-| "137" => f136
-| "138" => f137
-| "139" => f138
-| "140" => f139
-| "141" => f140
-| "142" => f141
-| "143" => f142
-| "144" => f143
-| "145" => f144
-| "146" => f145
-| "147" => f146
-| "148" => f147
-| "149" => f148
-| "150" => f149
-| "151" => f150
-| "152" => f151
-| "153" => f152
-| "154" => f153
-| "155" => f154
-| "156" => f155
-| "157" => f156
-| "158" => f157
-| "159" => f158
-| "160" => f159
-| "161" => f160
-| "162" => f161
-| "163" => f162
-| "164" => f163
-| "165" => f164
-| "166" => f165
-| "167" => f166
-| "168" => f167
-| "169" => f168
-| "170" => f169
-| "171" => f170
-| "172" => f171
-| "173" => f172
-| "174" => f173
-| "175" => f174
-| "176" => f175
-| "177" => f176
-| "178" => f177
-| "179" => f178
-| "180" => f179
-| "181" => f180
-| "182" => f181
-| "183" => f182
-| "184" => f183
-| "185" => f184
-| "186" => f185
-| "187" => f186
-| "188" => f187
-| "189" => f188
-| "190" => f189
-| "191" => f190
-| "192" => f191
-| "193" => f192
-| "194" => f193
-| "195" => f194
-| "196" => f195
-| "197" => f196
-| "198" => f197
-| "199" => f198
-| "200" => f199
-| "201" => f200
-| "202" => f201
-| "203" => f202
-| "204" => f203
-| "205" => f204
-| "206" => f205
-| "207" => f206
-| "208" => f207
-| "209" => f208
-| "210" => f209
-| "211" => f210
-| "212" => f211
-| "213" => f212
-| "214" => f213
-| "215" => f214
-| "216" => f215
-| "217" => f216
-| "218" => f217
-| "219" => f218
-| "220" => f219
-| "221" => f220
-| "222" => f221
-| "223" => f222
-| "224" => f223
-| "225" => f224
-| "226" => f225
-| "227" => f226
-| "228" => f227
-| "229" => f228
-| "230" => f229
-| "231" => f230
-| "232" => f231
-| "233" => f232
-| "234" => f233
-| "235" => f234
-| "236" => f235
-| "237" => f236
-| "238" => f237
-| "239" => f238
-| "240" => f239
-| "241" => f240
-| "242" => f241
-| "243" => f242
-| "244" => f243
-| "245" => f244
-| "246" => f245
-| "247" => f246
-| "248" => f247
-| "249" => f248
-| "250" => f249
-| "251" => f250
-| "252" => f251
-| "253" => f252
-| "254" => f253
-| "255" => f254
+| "000" => x00
+| "001" => x01
+| "002" => x02
+| "003" => x03
+| "004" => x04
+| "005" => x05
+| "006" => x06
+| "007" => x07
+| "008" => x08
+| "009" => x09
+| "010" => x0a
+| "011" => x0b
+| "012" => x0c
+| "013" => x0d
+| "014" => x0e
+| "015" => x0f
+| "016" => x10
+| "017" => x11
+| "018" => x12
+| "019" => x13
+| "020" => x14
+| "021" => x15
+| "022" => x16
+| "023" => x17
+| "024" => x18
+| "025" => x19
+| "026" => x1a
+| "027" => x1b
+| "028" => x1c
+| "029" => x1d
+| "030" => x1e
+| "031" => x1f
+| " " => x20
+| "!" => x21
+| """" => x22
+| "#" => x23
+| "$" => x24
+| "%" => x25
+| "&" => x26
+| "'" => x27
+| "(" => x28
+| ")" => x29
+| "*" => x2a
+| "+" => x2b
+| "," => x2c
+| "-" => x2d
+| "." => x2e
+| "/" => x2f
+| "0" => x30
+| "1" => x31
+| "2" => x32
+| "3" => x33
+| "4" => x34
+| "5" => x35
+| "6" => x36
+| "7" => x37
+| "8" => x38
+| "9" => x39
+| ":" => x3a
+| ";" => x3b
+| "<" => x3c
+| "=" => x3d
+| ">" => x3e
+| "?" => x3f
+| "@" => x40
+| "A" => x41
+| "B" => x42
+| "C" => x43
+| "D" => x44
+| "E" => x45
+| "F" => x46
+| "G" => x47
+| "H" => x48
+| "I" => x49
+| "J" => x4a
+| "K" => x4b
+| "L" => x4c
+| "M" => x4d
+| "N" => x4e
+| "O" => x4f
+| "P" => x50
+| "Q" => x51
+| "R" => x52
+| "S" => x53
+| "T" => x54
+| "U" => x55
+| "V" => x56
+| "W" => x57
+| "X" => x58
+| "Y" => x59
+| "Z" => x5a
+| "[" => x5b
+| "\" => x5c
+| "]" => x5d
+| "^" => x5e
+| "_" => x5f
+| "`" => x60
+| "a" => x61
+| "b" => x62
+| "c" => x63
+| "d" => x64
+| "e" => x65
+| "f" => x66
+| "g" => x67
+| "h" => x68
+| "i" => x69
+| "j" => x6a
+| "k" => x6b
+| "l" => x6c
+| "m" => x6d
+| "n" => x6e
+| "o" => x6f
+| "p" => x70
+| "q" => x71
+| "r" => x72
+| "s" => x73
+| "t" => x74
+| "u" => x75
+| "v" => x76
+| "w" => x77
+| "x" => x78
+| "y" => x79
+| "z" => x7a
+| "{" => x7b
+| "|" => x7c
+| "}" => x7d
+| "~" => x7e
+| "127" => x7f
+| "128" => x80
+| "129" => x81
+| "130" => x82
+| "131" => x83
+| "132" => x84
+| "133" => x85
+| "134" => x86
+| "135" => x87
+| "136" => x88
+| "137" => x89
+| "138" => x8a
+| "139" => x8b
+| "140" => x8c
+| "141" => x8d
+| "142" => x8e
+| "143" => x8f
+| "144" => x90
+| "145" => x91
+| "146" => x92
+| "147" => x93
+| "148" => x94
+| "149" => x95
+| "150" => x96
+| "151" => x97
+| "152" => x98
+| "153" => x99
+| "154" => x9a
+| "155" => x9b
+| "156" => x9c
+| "157" => x9d
+| "158" => x9e
+| "159" => x9f
+| "160" => xa0
+| "161" => xa1
+| "162" => xa2
+| "163" => xa3
+| "164" => xa4
+| "165" => xa5
+| "166" => xa6
+| "167" => xa7
+| "168" => xa8
+| "169" => xa9
+| "170" => xaa
+| "171" => xab
+| "172" => xac
+| "173" => xad
+| "174" => xae
+| "175" => xaf
+| "176" => xb0
+| "177" => xb1
+| "178" => xb2
+| "179" => xb3
+| "180" => xb4
+| "181" => xb5
+| "182" => xb6
+| "183" => xb7
+| "184" => xb8
+| "185" => xb9
+| "186" => xba
+| "187" => xbb
+| "188" => xbc
+| "189" => xbd
+| "190" => xbe
+| "191" => xbf
+| "192" => xc0
+| "193" => xc1
+| "194" => xc2
+| "195" => xc3
+| "196" => xc4
+| "197" => xc5
+| "198" => xc6
+| "199" => xc7
+| "200" => xc8
+| "201" => xc9
+| "202" => xca
+| "203" => xcb
+| "204" => xcc
+| "205" => xcd
+| "206" => xce
+| "207" => xcf
+| "208" => xd0
+| "209" => xd1
+| "210" => xd2
+| "211" => xd3
+| "212" => xd4
+| "213" => xd5
+| "214" => xd6
+| "215" => xd7
+| "216" => xd8
+| "217" => xd9
+| "218" => xda
+| "219" => xdb
+| "220" => xdc
+| "221" => xdd
+| "222" => xde
+| "223" => xdf
+| "224" => xe0
+| "225" => xe1
+| "226" => xe2
+| "227" => xe3
+| "228" => xe4
+| "229" => xe5
+| "230" => xe6
+| "231" => xe7
+| "232" => xe8
+| "233" => xe9
+| "234" => xea
+| "235" => xeb
+| "236" => xec
+| "237" => xed
+| "238" => xee
+| "239" => xef
+| "240" => xf0
+| "241" => xf1
+| "242" => xf2
+| "243" => xf3
+| "244" => xf4
+| "245" => xf5
+| "246" => xf6
+| "247" => xf7
+| "248" => xf8
+| "249" => xf9
+| "250" => xfa
+| "251" => xfb
+| "252" => xfc
+| "253" => xfd
+| "254" => xfe
+| "255" => xff
 end
      : forall P : byte -> Prop,
        P "000" ->
@@ -1045,8 +1045,8 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Arguments byte_ind P%_function_scope f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 
-  f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 b%_byte_scope
+Arguments byte_ind P%_function_scope x00 x01 x02 x03 x04 x05 x06 x07 x08 x09 x0a x0b x0c x0d x0e x0f x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x1a x1b x1c x1d x1e x1f x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x2a x2b x2c x2d x2e x2f x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x3a x3b x3c x3d x3e x3f x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x4a x4b x4c x4d x4e x4f x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x5a x5b x5c x5d x5e x5f x60 x61 x62 x63 x64 x65 x66 x67 x68 x69 x6a x6b x6c x6d x6e x6f x70 x71 x72 x73 x74 x75 x76 x77 x78 x79 x7a x7b x7c x7d x7e x7f x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x8a x8b x8c x8d x8e x8f x90 x91 x92 x93 x94 x95 x96 x97 x98 x99 x9a x9b x9c x9d x9e x9f xa0 xa1 xa2 xa3 xa4 xa5 xa6 xa7 xa8 xa9 xaa xab xac xad xae xaf xb0 xb1 xb2 xb3 xb4 xb5 xb6 xb7 xb8 xb9 xba xbb xbc xbd xbe xbf xc0 xc1 xc2 xc3 xc4 xc5 xc6 xc7 xc8 xc9 xca xcb xcc xcd xce xcf xd0 xd1 xd2 xd3 xd4 xd5 xd6 xd7 xd8 xd9 xda xdb xdc xdd xde xdf xe0 xe1 xe2 xe3 xe4 xe5 xe6 xe7 xe8 xe9 
+  xea xeb xec xed xee xef xf0 xf1 xf2 xf3 xf4 xf5 xf6 xf7 xf8 xf9 xfa xfb xfc xfd xfe xff b%_byte_scope
 "000"
      : byte
 "a"