Goal:
    b : byte
  ============================
   (forall e : NoConfusion_byte b b,
    noConfusion_byte_obligation_2 b b eq_refl = e)


DEBUG:Going to execute:
destruct b

Goals:
  
  ============================
   (forall e : NoConfusion_byte "000" "000",
    noConfusion_byte_obligation_2 "000" "000" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "001" "001",
    noConfusion_byte_obligation_2 "001" "001" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "002" "002",
    noConfusion_byte_obligation_2 "002" "002" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "003" "003",
    noConfusion_byte_obligation_2 "003" "003" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "004" "004",
    noConfusion_byte_obligation_2 "004" "004" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "005" "005",
    noConfusion_byte_obligation_2 "005" "005" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "006" "006",
    noConfusion_byte_obligation_2 "006" "006" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "007" "007",
    noConfusion_byte_obligation_2 "007" "007" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "008" "008",
    noConfusion_byte_obligation_2 "008" "008" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "009" "009",
    noConfusion_byte_obligation_2 "009" "009" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "010" "010",
    noConfusion_byte_obligation_2 "010" "010" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "011" "011",
    noConfusion_byte_obligation_2 "011" "011" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "012" "012",
    noConfusion_byte_obligation_2 "012" "012" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "013" "013",
    noConfusion_byte_obligation_2 "013" "013" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "014" "014",
    noConfusion_byte_obligation_2 "014" "014" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "015" "015",
    noConfusion_byte_obligation_2 "015" "015" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "016" "016",
    noConfusion_byte_obligation_2 "016" "016" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "017" "017",
    noConfusion_byte_obligation_2 "017" "017" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "018" "018",
    noConfusion_byte_obligation_2 "018" "018" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "019" "019",
    noConfusion_byte_obligation_2 "019" "019" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "020" "020",
    noConfusion_byte_obligation_2 "020" "020" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "021" "021",
    noConfusion_byte_obligation_2 "021" "021" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "022" "022",
    noConfusion_byte_obligation_2 "022" "022" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "023" "023",
    noConfusion_byte_obligation_2 "023" "023" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "024" "024",
    noConfusion_byte_obligation_2 "024" "024" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "025" "025",
    noConfusion_byte_obligation_2 "025" "025" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "026" "026",
    noConfusion_byte_obligation_2 "026" "026" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "027" "027",
    noConfusion_byte_obligation_2 "027" "027" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "028" "028",
    noConfusion_byte_obligation_2 "028" "028" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "029" "029",
    noConfusion_byte_obligation_2 "029" "029" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "030" "030",
    noConfusion_byte_obligation_2 "030" "030" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "031" "031",
    noConfusion_byte_obligation_2 "031" "031" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte " " " ",
    noConfusion_byte_obligation_2 " " " " eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "!" "!",
    noConfusion_byte_obligation_2 "!" "!" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte """" """",
    noConfusion_byte_obligation_2 """" """" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "#" "#",
    noConfusion_byte_obligation_2 "#" "#" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "$" "$",
    noConfusion_byte_obligation_2 "$" "$" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "%" "%",
    noConfusion_byte_obligation_2 "%" "%" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "&" "&",
    noConfusion_byte_obligation_2 "&" "&" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "'" "'",
    noConfusion_byte_obligation_2 "'" "'" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "(" "(",
    noConfusion_byte_obligation_2 "(" "(" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte ")" ")",
    noConfusion_byte_obligation_2 ")" ")" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "*" "*",
    noConfusion_byte_obligation_2 "*" "*" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "+" "+",
    noConfusion_byte_obligation_2 "+" "+" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "," ",",
    noConfusion_byte_obligation_2 "," "," eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "-" "-",
    noConfusion_byte_obligation_2 "-" "-" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "." ".",
    noConfusion_byte_obligation_2 "." "." eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "/" "/",
    noConfusion_byte_obligation_2 "/" "/" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "0" "0",
    noConfusion_byte_obligation_2 "0" "0" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "1" "1",
    noConfusion_byte_obligation_2 "1" "1" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "2" "2",
    noConfusion_byte_obligation_2 "2" "2" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "3" "3",
    noConfusion_byte_obligation_2 "3" "3" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "4" "4",
    noConfusion_byte_obligation_2 "4" "4" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "5" "5",
    noConfusion_byte_obligation_2 "5" "5" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "6" "6",
    noConfusion_byte_obligation_2 "6" "6" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "7" "7",
    noConfusion_byte_obligation_2 "7" "7" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "8" "8",
    noConfusion_byte_obligation_2 "8" "8" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "9" "9",
    noConfusion_byte_obligation_2 "9" "9" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte ":" ":",
    noConfusion_byte_obligation_2 ":" ":" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte ";" ";",
    noConfusion_byte_obligation_2 ";" ";" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "<" "<",
    noConfusion_byte_obligation_2 "<" "<" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "=" "=",
    noConfusion_byte_obligation_2 "=" "=" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte ">" ">",
    noConfusion_byte_obligation_2 ">" ">" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "?" "?",
    noConfusion_byte_obligation_2 "?" "?" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "@" "@",
    noConfusion_byte_obligation_2 "@" "@" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "A" "A",
    noConfusion_byte_obligation_2 "A" "A" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "B" "B",
    noConfusion_byte_obligation_2 "B" "B" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "C" "C",
    noConfusion_byte_obligation_2 "C" "C" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "D" "D",
    noConfusion_byte_obligation_2 "D" "D" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "E" "E",
    noConfusion_byte_obligation_2 "E" "E" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "F" "F",
    noConfusion_byte_obligation_2 "F" "F" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "G" "G",
    noConfusion_byte_obligation_2 "G" "G" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "H" "H",
    noConfusion_byte_obligation_2 "H" "H" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "I" "I",
    noConfusion_byte_obligation_2 "I" "I" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "J" "J",
    noConfusion_byte_obligation_2 "J" "J" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "K" "K",
    noConfusion_byte_obligation_2 "K" "K" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "L" "L",
    noConfusion_byte_obligation_2 "L" "L" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "M" "M",
    noConfusion_byte_obligation_2 "M" "M" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "N" "N",
    noConfusion_byte_obligation_2 "N" "N" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "O" "O",
    noConfusion_byte_obligation_2 "O" "O" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "P" "P",
    noConfusion_byte_obligation_2 "P" "P" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "Q" "Q",
    noConfusion_byte_obligation_2 "Q" "Q" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "R" "R",
    noConfusion_byte_obligation_2 "R" "R" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "S" "S",
    noConfusion_byte_obligation_2 "S" "S" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "T" "T",
    noConfusion_byte_obligation_2 "T" "T" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "U" "U",
    noConfusion_byte_obligation_2 "U" "U" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "V" "V",
    noConfusion_byte_obligation_2 "V" "V" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "W" "W",
    noConfusion_byte_obligation_2 "W" "W" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "X" "X",
    noConfusion_byte_obligation_2 "X" "X" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "Y" "Y",
    noConfusion_byte_obligation_2 "Y" "Y" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "Z" "Z",
    noConfusion_byte_obligation_2 "Z" "Z" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "[" "[",
    noConfusion_byte_obligation_2 "[" "[" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "\" "\",
    noConfusion_byte_obligation_2 "\" "\" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "]" "]",
    noConfusion_byte_obligation_2 "]" "]" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "^" "^",
    noConfusion_byte_obligation_2 "^" "^" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "_" "_",
    noConfusion_byte_obligation_2 "_" "_" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "`" "`",
    noConfusion_byte_obligation_2 "`" "`" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "a" "a",
    noConfusion_byte_obligation_2 "a" "a" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "b" "b",
    noConfusion_byte_obligation_2 "b" "b" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "c" "c",
    noConfusion_byte_obligation_2 "c" "c" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "d" "d",
    noConfusion_byte_obligation_2 "d" "d" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "e" "e",
    noConfusion_byte_obligation_2 "e" "e" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "f" "f",
    noConfusion_byte_obligation_2 "f" "f" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "g" "g",
    noConfusion_byte_obligation_2 "g" "g" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "h" "h",
    noConfusion_byte_obligation_2 "h" "h" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "i" "i",
    noConfusion_byte_obligation_2 "i" "i" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "j" "j",
    noConfusion_byte_obligation_2 "j" "j" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "k" "k",
    noConfusion_byte_obligation_2 "k" "k" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "l" "l",
    noConfusion_byte_obligation_2 "l" "l" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "m" "m",
    noConfusion_byte_obligation_2 "m" "m" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "n" "n",
    noConfusion_byte_obligation_2 "n" "n" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "o" "o",
    noConfusion_byte_obligation_2 "o" "o" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "p" "p",
    noConfusion_byte_obligation_2 "p" "p" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "q" "q",
    noConfusion_byte_obligation_2 "q" "q" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "r" "r",
    noConfusion_byte_obligation_2 "r" "r" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "s" "s",
    noConfusion_byte_obligation_2 "s" "s" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "t" "t",
    noConfusion_byte_obligation_2 "t" "t" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "u" "u",
    noConfusion_byte_obligation_2 "u" "u" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "v" "v",
    noConfusion_byte_obligation_2 "v" "v" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "w" "w",
    noConfusion_byte_obligation_2 "w" "w" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "x" "x",
    noConfusion_byte_obligation_2 "x" "x" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "y" "y",
    noConfusion_byte_obligation_2 "y" "y" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "z" "z",
    noConfusion_byte_obligation_2 "z" "z" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "{" "{",
    noConfusion_byte_obligation_2 "{" "{" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "|" "|",
    noConfusion_byte_obligation_2 "|" "|" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "}" "}",
    noConfusion_byte_obligation_2 "}" "}" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "~" "~",
    noConfusion_byte_obligation_2 "~" "~" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "127" "127",
    noConfusion_byte_obligation_2 "127" "127" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "128" "128",
    noConfusion_byte_obligation_2 "128" "128" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "129" "129",
    noConfusion_byte_obligation_2 "129" "129" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "130" "130",
    noConfusion_byte_obligation_2 "130" "130" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "131" "131",
    noConfusion_byte_obligation_2 "131" "131" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "132" "132",
    noConfusion_byte_obligation_2 "132" "132" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "133" "133",
    noConfusion_byte_obligation_2 "133" "133" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "134" "134",
    noConfusion_byte_obligation_2 "134" "134" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "135" "135",
    noConfusion_byte_obligation_2 "135" "135" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "136" "136",
    noConfusion_byte_obligation_2 "136" "136" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "137" "137",
    noConfusion_byte_obligation_2 "137" "137" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "138" "138",
    noConfusion_byte_obligation_2 "138" "138" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "139" "139",
    noConfusion_byte_obligation_2 "139" "139" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "140" "140",
    noConfusion_byte_obligation_2 "140" "140" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "141" "141",
    noConfusion_byte_obligation_2 "141" "141" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "142" "142",
    noConfusion_byte_obligation_2 "142" "142" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "143" "143",
    noConfusion_byte_obligation_2 "143" "143" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "144" "144",
    noConfusion_byte_obligation_2 "144" "144" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "145" "145",
    noConfusion_byte_obligation_2 "145" "145" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "146" "146",
    noConfusion_byte_obligation_2 "146" "146" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "147" "147",
    noConfusion_byte_obligation_2 "147" "147" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "148" "148",
    noConfusion_byte_obligation_2 "148" "148" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "149" "149",
    noConfusion_byte_obligation_2 "149" "149" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "150" "150",
    noConfusion_byte_obligation_2 "150" "150" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "151" "151",
    noConfusion_byte_obligation_2 "151" "151" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "152" "152",
    noConfusion_byte_obligation_2 "152" "152" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "153" "153",
    noConfusion_byte_obligation_2 "153" "153" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "154" "154",
    noConfusion_byte_obligation_2 "154" "154" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "155" "155",
    noConfusion_byte_obligation_2 "155" "155" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "156" "156",
    noConfusion_byte_obligation_2 "156" "156" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "157" "157",
    noConfusion_byte_obligation_2 "157" "157" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "158" "158",
    noConfusion_byte_obligation_2 "158" "158" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "159" "159",
    noConfusion_byte_obligation_2 "159" "159" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "160" "160",
    noConfusion_byte_obligation_2 "160" "160" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "161" "161",
    noConfusion_byte_obligation_2 "161" "161" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "162" "162",
    noConfusion_byte_obligation_2 "162" "162" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "163" "163",
    noConfusion_byte_obligation_2 "163" "163" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "164" "164",
    noConfusion_byte_obligation_2 "164" "164" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "165" "165",
    noConfusion_byte_obligation_2 "165" "165" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "166" "166",
    noConfusion_byte_obligation_2 "166" "166" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "167" "167",
    noConfusion_byte_obligation_2 "167" "167" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "168" "168",
    noConfusion_byte_obligation_2 "168" "168" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "169" "169",
    noConfusion_byte_obligation_2 "169" "169" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "170" "170",
    noConfusion_byte_obligation_2 "170" "170" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "171" "171",
    noConfusion_byte_obligation_2 "171" "171" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "172" "172",
    noConfusion_byte_obligation_2 "172" "172" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "173" "173",
    noConfusion_byte_obligation_2 "173" "173" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "174" "174",
    noConfusion_byte_obligation_2 "174" "174" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "175" "175",
    noConfusion_byte_obligation_2 "175" "175" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "176" "176",
    noConfusion_byte_obligation_2 "176" "176" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "177" "177",
    noConfusion_byte_obligation_2 "177" "177" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "178" "178",
    noConfusion_byte_obligation_2 "178" "178" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "179" "179",
    noConfusion_byte_obligation_2 "179" "179" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "180" "180",
    noConfusion_byte_obligation_2 "180" "180" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "181" "181",
    noConfusion_byte_obligation_2 "181" "181" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "182" "182",
    noConfusion_byte_obligation_2 "182" "182" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "183" "183",
    noConfusion_byte_obligation_2 "183" "183" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "184" "184",
    noConfusion_byte_obligation_2 "184" "184" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "185" "185",
    noConfusion_byte_obligation_2 "185" "185" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "186" "186",
    noConfusion_byte_obligation_2 "186" "186" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "187" "187",
    noConfusion_byte_obligation_2 "187" "187" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "188" "188",
    noConfusion_byte_obligation_2 "188" "188" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "189" "189",
    noConfusion_byte_obligation_2 "189" "189" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "190" "190",
    noConfusion_byte_obligation_2 "190" "190" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "191" "191",
    noConfusion_byte_obligation_2 "191" "191" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "192" "192",
    noConfusion_byte_obligation_2 "192" "192" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "193" "193",
    noConfusion_byte_obligation_2 "193" "193" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "194" "194",
    noConfusion_byte_obligation_2 "194" "194" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "195" "195",
    noConfusion_byte_obligation_2 "195" "195" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "196" "196",
    noConfusion_byte_obligation_2 "196" "196" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "197" "197",
    noConfusion_byte_obligation_2 "197" "197" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "198" "198",
    noConfusion_byte_obligation_2 "198" "198" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "199" "199",
    noConfusion_byte_obligation_2 "199" "199" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "200" "200",
    noConfusion_byte_obligation_2 "200" "200" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "201" "201",
    noConfusion_byte_obligation_2 "201" "201" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "202" "202",
    noConfusion_byte_obligation_2 "202" "202" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "203" "203",
    noConfusion_byte_obligation_2 "203" "203" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "204" "204",
    noConfusion_byte_obligation_2 "204" "204" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "205" "205",
    noConfusion_byte_obligation_2 "205" "205" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "206" "206",
    noConfusion_byte_obligation_2 "206" "206" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "207" "207",
    noConfusion_byte_obligation_2 "207" "207" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "208" "208",
    noConfusion_byte_obligation_2 "208" "208" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "209" "209",
    noConfusion_byte_obligation_2 "209" "209" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "210" "210",
    noConfusion_byte_obligation_2 "210" "210" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "211" "211",
    noConfusion_byte_obligation_2 "211" "211" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "212" "212",
    noConfusion_byte_obligation_2 "212" "212" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "213" "213",
    noConfusion_byte_obligation_2 "213" "213" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "214" "214",
    noConfusion_byte_obligation_2 "214" "214" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "215" "215",
    noConfusion_byte_obligation_2 "215" "215" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "216" "216",
    noConfusion_byte_obligation_2 "216" "216" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "217" "217",
    noConfusion_byte_obligation_2 "217" "217" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "218" "218",
    noConfusion_byte_obligation_2 "218" "218" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "219" "219",
    noConfusion_byte_obligation_2 "219" "219" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "220" "220",
    noConfusion_byte_obligation_2 "220" "220" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "221" "221",
    noConfusion_byte_obligation_2 "221" "221" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "222" "222",
    noConfusion_byte_obligation_2 "222" "222" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "223" "223",
    noConfusion_byte_obligation_2 "223" "223" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "224" "224",
    noConfusion_byte_obligation_2 "224" "224" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "225" "225",
    noConfusion_byte_obligation_2 "225" "225" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "226" "226",
    noConfusion_byte_obligation_2 "226" "226" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "227" "227",
    noConfusion_byte_obligation_2 "227" "227" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "228" "228",
    noConfusion_byte_obligation_2 "228" "228" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "229" "229",
    noConfusion_byte_obligation_2 "229" "229" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "230" "230",
    noConfusion_byte_obligation_2 "230" "230" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "231" "231",
    noConfusion_byte_obligation_2 "231" "231" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "232" "232",
    noConfusion_byte_obligation_2 "232" "232" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "233" "233",
    noConfusion_byte_obligation_2 "233" "233" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "234" "234",
    noConfusion_byte_obligation_2 "234" "234" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "235" "235",
    noConfusion_byte_obligation_2 "235" "235" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "236" "236",
    noConfusion_byte_obligation_2 "236" "236" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "237" "237",
    noConfusion_byte_obligation_2 "237" "237" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "238" "238",
    noConfusion_byte_obligation_2 "238" "238" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "239" "239",
    noConfusion_byte_obligation_2 "239" "239" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "240" "240",
    noConfusion_byte_obligation_2 "240" "240" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "241" "241",
    noConfusion_byte_obligation_2 "241" "241" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "242" "242",
    noConfusion_byte_obligation_2 "242" "242" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "243" "243",
    noConfusion_byte_obligation_2 "243" "243" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "244" "244",
    noConfusion_byte_obligation_2 "244" "244" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "245" "245",
    noConfusion_byte_obligation_2 "245" "245" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "246" "246",
    noConfusion_byte_obligation_2 "246" "246" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "247" "247",
    noConfusion_byte_obligation_2 "247" "247" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "248" "248",
    noConfusion_byte_obligation_2 "248" "248" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "249" "249",
    noConfusion_byte_obligation_2 "249" "249" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "250" "250",
    noConfusion_byte_obligation_2 "250" "250" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "251" "251",
    noConfusion_byte_obligation_2 "251" "251" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "252" "252",
    noConfusion_byte_obligation_2 "252" "252" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "253" "253",
    noConfusion_byte_obligation_2 "253" "253" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "254" "254",
    noConfusion_byte_obligation_2 "254" "254" eq_refl = e)

  
  ============================
   (forall e : NoConfusion_byte "255" "255",
    noConfusion_byte_obligation_2 "255" "255" eq_refl = e)


DEBUG:Going to execute:
vm_compute
DEBUG LTAC Evaluated term: b

Goals:
  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)

  
  ============================
   (forall x : True, I = x)


DEBUG:Going to execute:
intros []

Goals:
  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)


DEBUG:Going to execute:
reflexivity

Goals:
  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)

  
  ============================
   (I = I)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>