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


DEBUG:Going to execute:
t; easy
Level 2: evaluation returns
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
where
H := Hcomp
of type
constr of type tacvalue

Level 1: evaluation returns
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
where
H := Hcomp
of type
constr of type tacvalue