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_
  ============================
   (weight (to_pathOf Gl p) = Z.of_nat (l _y_) - Z.of_nat (l _x_))


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrapply@0> $1
DEBUG LTAC Evaluated term: sweight_weight
DEBUG LTAC Evaluated term: sweight_weight