Goal:
    G : t  z : V.t  s : VSet.t  x : V.t  H : VSet.mem x s = false
  ============================
   (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.ssreflect::ssrrewrite@0> $1 $2
DEBUG LTAC Evaluated term: (H x)
DEBUG LTAC Evaluated term: VSetProp.FM.not_mem_iff