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) => 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 end : forall P : byte -> Type, P "000" -> P "001" -> P "002" -> P "003" -> P "004" -> P "005" -> P "006" -> P "007" -> P "008" -> P "009" -> P "010" -> P "011" -> P "012" -> P "013" -> P "014" -> P "015" -> P "016" -> P "017" -> P "018" -> P "019" -> P "020" -> P "021" -> P "022" -> P "023" -> P "024" -> P "025" -> P "026" -> P "027" -> P "028" -> P "029" -> P "030" -> P "031" -> P " " -> P "!" -> P """" -> P "#" -> P "$" -> P "%" -> P "&" -> P "'" -> P "(" -> P ")" -> P "*" -> P "+" -> P "," -> P "-" -> P "." -> P "/" -> P "0" -> P "1" -> P "2" -> P "3" -> P "4" -> P "5" -> P "6" -> P "7" -> P "8" -> P "9" -> P ":" -> P ";" -> P "<" -> P "=" -> P ">" -> P "?" -> P "@" -> P "A" -> P "B" -> P "C" -> P "D" -> P "E" -> P "F" -> P "G" -> P "H" -> P "I" -> P "J" -> P "K" -> P "L" -> P "M" -> P "N" -> P "O" -> P "P" -> P "Q" -> P "R" -> P "S" -> P "T" -> P "U" -> P "V" -> P "W" -> P "X" -> P "Y" -> P "Z" -> P "[" -> P "\" -> P "]" -> P "^" -> P "_" -> P "`" -> P "a" -> P "b" -> P "c" -> P "d" -> P "e" -> P "f" -> P "g" -> P "h" -> P "i" -> P "j" -> P "k" -> P "l" -> P "m" -> P "n" -> P "o" -> P "p" -> P "q" -> P "r" -> P "s" -> P "t" -> P "u" -> P "v" -> P "w" -> P "x" -> P "y" -> P "z" -> P "{" -> P "|" -> P "}" -> P "~" -> P "127" -> P "128" -> P "129" -> P "130" -> P "131" -> P "132" -> P "133" -> P "134" -> P "135" -> P "136" -> P "137" -> P "138" -> P "139" -> P "140" -> P "141" -> P "142" -> P "143" -> P "144" -> P "145" -> P "146" -> P "147" -> P "148" -> P "149" -> P "150" -> P "151" -> P "152" -> P "153" -> P "154" -> P "155" -> P "156" -> P "157" -> P "158" -> P "159" -> P "160" -> P "161" -> P "162" -> P "163" -> P "164" -> P "165" -> P "166" -> 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 _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, P "000" -> P "001" -> P "002" -> P "003" -> P "004" -> P "005" -> P "006" -> P "007" -> P "008" -> P "009" -> P "010" -> P "011" -> P "012" -> P "013" -> P "014" -> P "015" -> P "016" -> P "017" -> P "018" -> P "019" -> P "020" -> P "021" -> P "022" -> P "023" -> P "024" -> P "025" -> P "026" -> P "027" -> P "028" -> P "029" -> P "030" -> P "031" -> P " " -> P "!" -> P """" -> P "#" -> P "$" -> P "%" -> P "&" -> P "'" -> P "(" -> P ")" -> P "*" -> P "+" -> P "," -> P "-" -> P "." -> P "/" -> P "0" -> P "1" -> P "2" -> P "3" -> P "4" -> P "5" -> P "6" -> P "7" -> P "8" -> P "9" -> P ":" -> P ";" -> P "<" -> P "=" -> P ">" -> P "?" -> P "@" -> P "A" -> P "B" -> P "C" -> P "D" -> P "E" -> P "F" -> P "G" -> P "H" -> P "I" -> P "J" -> P "K" -> P "L" -> P "M" -> P "N" -> P "O" -> P "P" -> P "Q" -> P "R" -> P "S" -> P "T" -> P "U" -> P "V" -> P "W" -> P "X" -> P "Y" -> P "Z" -> P "[" -> P "\" -> P "]" -> P "^" -> P "_" -> P "`" -> P "a" -> P "b" -> P "c" -> P "d" -> P "e" -> P "f" -> P "g" -> P "h" -> P "i" -> P "j" -> P "k" -> P "l" -> P "m" -> P "n" -> P "o" -> P "p" -> P "q" -> P "r" -> P "s" -> P "t" -> P "u" -> P "v" -> P "w" -> P "x" -> P "y" -> P "z" -> P "{" -> P "|" -> P "}" -> P "~" -> P "127" -> P "128" -> P "129" -> P "130" -> P "131" -> P "132" -> P "133" -> P "134" -> P "135" -> P "136" -> P "137" -> P "138" -> P "139" -> P "140" -> P "141" -> P "142" -> P "143" -> P "144" -> P "145" -> P "146" -> P "147" -> P "148" -> P "149" -> P "150" -> P "151" -> P "152" -> P "153" -> P "154" -> P "155" -> P "156" -> P "157" -> P "158" -> P "159" -> P "160" -> P "161" -> P "162" -> P "163" -> P "164" -> P "165" -> P "166" -> 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 _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%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) => 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 end : forall P : byte -> Prop, P "000" -> P "001" -> P "002" -> P "003" -> P "004" -> P "005" -> P "006" -> P "007" -> P "008" -> P "009" -> P "010" -> P "011" -> P "012" -> P "013" -> P "014" -> P "015" -> P "016" -> P "017" -> P "018" -> P "019" -> P "020" -> P "021" -> P "022" -> P "023" -> P "024" -> P "025" -> P "026" -> P "027" -> P "028" -> P "029" -> P "030" -> P "031" -> P " " -> P "!" -> P """" -> P "#" -> P "$" -> P "%" -> P "&" -> P "'" -> P "(" -> P ")" -> P "*" -> P "+" -> P "," -> P "-" -> P "." -> P "/" -> P "0" -> P "1" -> P "2" -> P "3" -> P "4" -> P "5" -> P "6" -> P "7" -> P "8" -> P "9" -> P ":" -> P ";" -> P "<" -> P "=" -> P ">" -> P "?" -> P "@" -> P "A" -> P "B" -> P "C" -> P "D" -> P "E" -> P "F" -> P "G" -> P "H" -> P "I" -> P "J" -> P "K" -> P "L" -> P "M" -> P "N" -> P "O" -> P "P" -> P "Q" -> P "R" -> P "S" -> P "T" -> P "U" -> P "V" -> P "W" -> P "X" -> P "Y" -> P "Z" -> P "[" -> P "\" -> P "]" -> P "^" -> P "_" -> P "`" -> P "a" -> P "b" -> P "c" -> P "d" -> P "e" -> P "f" -> P "g" -> P "h" -> P "i" -> P "j" -> P "k" -> P "l" -> P "m" -> P "n" -> P "o" -> P "p" -> P "q" -> P "r" -> P "s" -> P "t" -> P "u" -> P "v" -> P "w" -> P "x" -> P "y" -> P "z" -> P "{" -> P "|" -> P "}" -> P "~" -> P "127" -> P "128" -> P "129" -> P "130" -> P "131" -> P "132" -> P "133" -> P "134" -> P "135" -> P "136" -> P "137" -> P "138" -> P "139" -> P "140" -> P "141" -> P "142" -> P "143" -> P "144" -> P "145" -> P "146" -> P "147" -> P "148" -> P "149" -> P "150" -> P "151" -> P "152" -> P "153" -> P "154" -> P "155" -> P "156" -> P "157" -> P "158" -> P "159" -> P "160" -> P "161" -> P "162" -> P "163" -> P "164" -> P "165" -> P "166" -> 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 _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope "000" : byte "a" : byte "127" : byte The command has indeed failed with message: Expects a single character or a three-digit ASCII code. "000" : ascii "a" : ascii "127" : ascii The command has indeed failed with message: Expects a single character or a three-digit ASCII code. "000" : string "a" : string "127" : string "€" : string "" : string = "a"%char : ascii = "a"%byte : byte = "a"%string : string = ["a"%byte] : list byte = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167"; "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"] : list byte = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167"; "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"] : list ascii "abc" : string "000" : nat "001" : nat "002" : nat "255" : nat The command has indeed failed with message: Expects a single character or a three-digit ASCII code. "abc" : string2 "abc" : string2 : string2 "abc" : string1 : string1