Goal:
    G : t  s : VSet.t  s' : VSet.t  x : V.t  y : V.t
  ============================
   ((fun t : Nbar.t =>
     lsp0 s x y = t -> VSet.Subset s s' -> (t <= lsp0 s' x y)%nbar)
      (lsp0 s x y))


DEBUG:Going to execute:
case x
DEBUG LTAC Evaluated term: (lsp0 s x y)