Goal:
    G : t  s : VSet.t  x : V.t  n : Z  lspeq : lsp0 s x x = Some n
  ============================
   ((Some (sweight (spath_refl s x)) <= lsp0 s x x)%nbar -> 0 <= n)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2
DEBUG LTAC Evaluated term: (lsp0_spec_le (spath_refl s x))