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
  ============================
   (EdgeSet.fold
      (fun '(src, w, tgt) (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) (E G) (if is_left (V.eq_dec x z) then Some 0 else None) =
    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))


DEBUG:Going to execute:
case not_locked_false_eq_true; Ltac.assumption
Level 1: Backtrace:

In environment
G : t
fuel : nat
s : VSet.t
x, z : V.t
IHfuel : forall (s : VSet.t) (x z : V.t),
         lsp00_fast fuel s x z = lsp00 fuel s x z
Unable to unify
 "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)"
with
 "EdgeSet.fold
    (fun '(src, w, tgt) (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) (E G) (if is_left (V.eq_dec x z) then Some 0 else None)".
Level 0: Backtrace:

In environment
G : t
fuel : nat
s : VSet.t
x, z : V.t
IHfuel : forall (s : VSet.t) (x z : V.t),
         lsp00_fast fuel s x z = lsp00 fuel s x z
Unable to unify
 "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)"
with
 "EdgeSet.fold
    (fun '(src, w, tgt) (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) (E G) (if is_left (V.eq_dec x z) then Some 0 else None)".
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.