Goal:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  _x_ : V.t
  _y_ : V.t
  _n_ : Z
  p : SPath Gl (V Gl) _x_ _y_
  ============================
   (sweight p = Z.of_nat (l _y_) - Z.of_nat (l _x_))


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2
DEBUG LTAC Evaluated term: lsp0_spec_eq
DEBUG LTAC Evaluated term: (lsp0_spec_eq ?t ?z ?e)
DEBUG LTAC Evaluated term: (lsp0_spec_eq Gl _n_ _view_subject_)