Goal:
    G : t  fuel : nat  s : VSet.t  x : V.t  z : V.t
  ============================
   (lsp00_fast fuel s x z = lsp00 fuel s x z)


DEBUG:Going to execute:
induction fuel in s, x, z |- *

Goals:
    G : t  s : VSet.t  x : V.t  z : V.t
  ============================
   (lsp00_fast 0 s x z = lsp00 0 s x z)

  
  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
  ============================
   (lsp00_fast (Datatypes.S fuel) s x z = lsp00 (Datatypes.S fuel) s x z)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: fuel

Goals:
    G : t  s : VSet.t  x : V.t  z : V.t
  ============================
   (lsp00_fast 0 s x z = lsp00 0 s x z)

  
  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
  ============================
   (lsp00_fast (Datatypes.S fuel) s x z = lsp00 (Datatypes.S fuel) s x z)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3