Goal:
    G : t  s : VSet.t  x : V.t  z : V.t  fuel := VSet.cardinal s : nat
  ============================
   (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:
cut (VSet.cardinal s = fuel)
DEBUG LTAC Evaluated term: (VSet.cardinal s)