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
  ============================
   ((if is_left (V.eq_dec x z) then Some 0 else None) =
    (if is_left (V.eq_dec x z) then Some 0 else None))


DEBUG:Going to execute:
trivial; hnf