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
  ============================
   (fold_left
      (fun (a : Nbar.t) (e : EdgeSet.elt) =>
       (let
        '(src, w, tgt) := e in
         fun acc : Nbar.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) a) (EdgeSet.elements (E G))
      (if is_left (V.eq_dec x z) then Some 0 else None) =
    fold_left
      (fun (acc : Nbar.t) (x0 : Edge.t) =>
       max acc (Some x0..w + lsp00 fuel (VSet.remove x s) x0..t z))
      (filter (fun e : Edge.t => V.eq_dec e..s x) (EdgeSet.elements (E G)))
      (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: fold_left_map
DEBUG LTAC Evaluated term: fold_left_map