Goal:
  
  ============================
   (forall (a b : byte) (e : a = b),
    (fun (a0 b0 : byte) (H : NoConfusion_byte a0 b0) =>
     noConfusion_byte_obligation_1 a0 b0 H) a b
      ((fun (a0 b0 : byte) (H : a0 = b0) =>
        noConfusion_byte_obligation_2 a0 b0 H) a b e) = e)


DEBUG:Going to execute:
simpl in *; Tactics.program_simplify