Goal:
  
  ============================
   nat


DEBUG:Going to execute:
let __ := open_constr:((eq_refl : ev = S _)) in
           refine
           0
Level 2: ev
 has value 
?y