Goal:
  
  ============================
   (list Byte.byte)


DEBUG:Going to execute:
exact ls
DEBUG LTAC Evaluated term: (flat_map
                              (fun v : nat =>
                               match Byte.of_nat v with
                               | Some v0 => [v0]
                               | None => []
                               end) (seq 0 256))
DEBUG LTAC Evaluated term: [Byte.x00; Byte.x01; Byte.x02; Byte.x03; Byte.x04;
                            Byte.x05; Byte.x06; Byte.x07; Byte.x08; Byte.x09;
                            Byte.x0a; Byte.x0b; Byte.x0c; Byte.x0d; Byte.x0e;
                            Byte.x0f; Byte.x10; Byte.x11; Byte.x12; Byte.x13;
                            Byte.x14; Byte.x15; Byte.x16; Byte.x17; Byte.x18;
                            Byte.x19; Byte.x1a; Byte.x1b; Byte.x1c; Byte.x1d;
                            Byte.x1e; Byte.x1f; Byte.x20; Byte.x21; Byte.x22;
                            Byte.x23; Byte.x24; Byte.x25; Byte.x26; Byte.x27;
                            Byte.x28; Byte.x29; Byte.x2a; Byte.x2b; Byte.x2c;
                            Byte.x2d; Byte.x2e; Byte.x2f; Byte.x30; Byte.x31;
                            Byte.x32; Byte.x33; Byte.x34; Byte.x35; Byte.x36;
                            Byte.x37; Byte.x38; Byte.x39; Byte.x3a; Byte.x3b;
                            Byte.x3c; Byte.x3d; Byte.x3e; Byte.x3f; Byte.x40;
                            Byte.x41; Byte.x42; Byte.x43; Byte.x44; Byte.x45;
                            Byte.x46; Byte.x47; Byte.x48; Byte.x49; Byte.x4a;
                            Byte.x4b; Byte.x4c; Byte.x4d; Byte.x4e; Byte.x4f;
                            Byte.x50; Byte.x51; Byte.x52; Byte.x53; Byte.x54;
                            Byte.x55; Byte.x56; Byte.x57; Byte.x58; Byte.x59;
                            Byte.x5a; Byte.x5b; Byte.x5c; Byte.x5d; Byte.x5e;
                            Byte.x5f; Byte.x60; Byte.x61; Byte.x62; Byte.x63;
                            Byte.x64; Byte.x65; Byte.x66; Byte.x67; Byte.x68;
                            Byte.x69; Byte.x6a; Byte.x6b; Byte.x6c; Byte.x6d;
                            Byte.x6e; Byte.x6f; Byte.x70; Byte.x71; Byte.x72;
                            Byte.x73; Byte.x74; Byte.x75; Byte.x76; Byte.x77;
                            Byte.x78; Byte.x79; Byte.x7a; Byte.x7b; Byte.x7c;
                            Byte.x7d; Byte.x7e; Byte.x7f; Byte.x80; Byte.x81;
                            Byte.x82; Byte.x83; Byte.x84; Byte.x85; Byte.x86;
                            Byte.x87; Byte.x88; Byte.x89; Byte.x8a; Byte.x8b;
                            Byte.x8c; Byte.x8d; Byte.x8e; Byte.x8f; Byte.x90;
                            Byte.x91; Byte.x92; Byte.x93; Byte.x94; Byte.x95;
                            Byte.x96; Byte.x97; Byte.x98; Byte.x99; Byte.x9a;
                            Byte.x9b; Byte.x9c; Byte.x9d; Byte.x9e; Byte.x9f;
                            Byte.xa0; Byte.xa1; Byte.xa2; Byte.xa3; Byte.xa4;
                            Byte.xa5; Byte.xa6; Byte.xa7; Byte.xa8; Byte.xa9;
                            Byte.xaa; Byte.xab; Byte.xac; Byte.xad; Byte.xae;
                            Byte.xaf; Byte.xb0; Byte.xb1; Byte.xb2; Byte.xb3;
                            Byte.xb4; Byte.xb5; Byte.xb6; Byte.xb7; Byte.xb8;
                            Byte.xb9; Byte.xba; Byte.xbb; Byte.xbc; Byte.xbd;
                            Byte.xbe; Byte.xbf; Byte.xc0; Byte.xc1; Byte.xc2;
                            Byte.xc3; Byte.xc4; Byte.xc5; Byte.xc6; Byte.xc7;
                            Byte.xc8; Byte.xc9; Byte.xca; Byte.xcb; Byte.xcc;
                            Byte.xcd; Byte.xce; Byte.xcf; Byte.xd0; Byte.xd1;
                            Byte.xd2; Byte.xd3; Byte.xd4; Byte.xd5; Byte.xd6;
                            Byte.xd7; Byte.xd8; Byte.xd9; Byte.xda; Byte.xdb;
                            Byte.xdc; Byte.xdd; Byte.xde; Byte.xdf; Byte.xe0;
                            Byte.xe1; Byte.xe2; Byte.xe3; Byte.xe4; Byte.xe5;
                            Byte.xe6; Byte.xe7; Byte.xe8; Byte.xe9; Byte.xea;
                            Byte.xeb; Byte.xec; Byte.xed; Byte.xee; Byte.xef;
                            Byte.xf0; Byte.xf1; Byte.xf2; Byte.xf3; Byte.xf4;
                            Byte.xf5; Byte.xf6; Byte.xf7; Byte.xf8; Byte.xf9;
                            Byte.xfa; Byte.xfb; Byte.xfc; Byte.xfd; Byte.xfe;
                            Byte.xff]