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:
reflexivity
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: H