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:
subst
DEBUG LTAC Evaluated term: edge_map_spec2
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=exists e0 : Edge.t,
                                    (_x_, _x1_, _y_) =
                                    (fun e : Edge.t =>
                                     (e..s, diff l e..s e..t, e..t)) e0 /\
                                    EdgeSet.In e0 (E G))
                              (edge_map_spec2
                                 (fun e : Edge.t =>
                                  (e..s, diff l e..s e..t, e..t)) 
                                 (E G) (_x_, _x1_, _y_)) _view_subject_)