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
  ============================
   (max acc (Some w + lsp00_fast fuel (VSet.remove x s) tgt z) =
    max acc (Some w + lsp00 fuel (VSet.remove x s) tgt z))


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
acc : Nbar.t
src : V.t
w : Z
tgt : V.t
Unable to unify "max acc (Some w + lsp00 fuel (VSet.remove x s) tgt z)" with
 "max acc (Some w + lsp00_fast fuel (VSet.remove x s) tgt z)".
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
acc : Nbar.t
src : V.t
w : Z
tgt : V.t
Unable to unify "max acc (Some w + lsp00 fuel (VSet.remove x s) tgt z)" with
 "max acc (Some w + lsp00_fast fuel (VSet.remove x s) tgt z)".
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.