Goal:
  
  G : t
  z : V.t
  fuel : nat
  IHfuel : forall (s : VSet.t) (x : V.t),
           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)
  s : VSet.t
  x : V.t
  H : VSet.cardinal s = Datatypes.S fuel
  ============================
   ((if VSet.mem x s
     then
      fold_left max
        (map
           (fun '(n, y) => (Some n + lsp00 fuel (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) =
    (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:
generalize eq_refl; pattern x at - 1
Level 1: evaluation returns
generalize eq_refl; pattern x at - 1; case x
where
x := VSet.mem x s
of type
constr of type tacvalue