Goal:
    G : t  s : VSet.t  x : V.t  z : V.t  fuel := VSet.cardinal s : nat
  ============================
   (VSet.cardinal s = fuel ->
    lsp00 fuel s x z =
    (if VSet.mem x s
     then
      fold_left max
        (map
           (fun '(n, y) =>
            (Some n +
             lsp00 (VSet.cardinal (VSet.remove x s)) (VSet.remove x s) y z)%nbar)
           (succs x)) (if is_left (V.eq_dec x z) then Some 0 else None)
     else if is_left (V.eq_dec x z) then Some 0 else None))


DEBUG:Going to execute:
idtac
Level 1: evaluation returns
<coq-core.plugins.ltac::cut@0>
where
$1 := VSet.cardinal s = fuel
of type
constr of type tacvalue