Goal:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  _y_ : V.t
  _z_ : V.t
  _x1_ : Z
  _x2_ : Edge.t
  _Hyp_ : _x_ = _x2_..s
  _Hyp1_ : _x1_ = diff l _x2_..s _x2_..t
  _Hyp2_ : _y_ = _x2_..t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _y_ _z_
  ============================
   (_x1_ + (Z.of_nat (l _z_) - Z.of_nat (l _y_)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x_))


DEBUG:Going to execute:
<coq-core.plugins.ltac::subst@1>