Goal:
    G : t  z : V.t  s : VSet.t  x : V.t  H : VSet.mem x s = false
  ============================
   (lsp00 0 s x z = (if is_left (V.eq_dec x z) then Some 0 else None))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>