Goal:
    G : t  z : V.t  s : VSet.t  x : V.t  H : VSet.Empty s
  ============================
   (lsp00 0 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:
<coq-core.plugins.ltac::specialize@0> $1
DEBUG LTAC Evaluated term: fuel
DEBUG LTAC Evaluated term: VSetProp.cardinal_inv_1