Goal:
    b : byte
  ============================
   (noConfusion_byte_obligation_1 b b
      (noConfusion_byte_obligation_2 b b eq_refl) = eq_refl)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: (noConfusion_byte_obligation_1 b b
                              (noConfusion_byte_obligation_2 b b eq_refl) =
                            eq_refl)
DEBUG LTAC Evaluated term: Prop
Level 3: type of T
 has value 
Prop