Goal:
    x : byte  y : byte  Hcomp : Some x = Some y
  ============================
   (x = y)


DEBUG:Going to execute:
CoreTactics.block_goal; CoreTactics.revert_until H;
            CoreTactics.block_goal;
            CoreTactics.on_last_hyp ltac:(fun H' => revert H');
            DepElim.simplify_dep_elim; CoreTactics.intros_until_block;
            CoreTactics.intros_until_block