Goal:
  
  G : t
  fuel : nat
  s : VSet.t
  x : V.t
  z : V.t
  IHfuel : forall (s : VSet.t) (x z : V.t),
           lsp00_fast fuel s x z = lsp00 fuel s x z
  acc : Nbar.t
  src : V.t
  w : Z
  tgt : V.t
  ============================
   ((if is_left (V.eq_dec src x)
     then max acc (Some w + lsp00_fast fuel (VSet.remove x s) tgt z)
     else acc) =
    (if is_left (V.eq_dec (src, w, tgt)..s x)
     then
      max acc
        (Some (src, w, tgt)..w +
         lsp00 fuel (VSet.remove x s) (src, w, tgt)..t z)
     else acc))


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: fold_left_proper