Goal:
  
  G : t
  l : labelling
  Hl : forall e : EdgeSet.elt,
       EdgeSet.In e (E G) -> Z.of_nat (l e..s) + e..w <= Z.of_nat (l e..t)
  x : V.t
  y : V.t
  z : V.t
  e : EdgeOf x y
  p : PathOf y z
  IHp : Z.of_nat (l y) + weight p <= Z.of_nat (l z)
  ============================
   (Z.of_nat (l x) + weight (pathOf_step e p) <= Z.of_nat (l z))


DEBUG:Going to execute:
<coq-core.plugins.ltac::specialize@0> $1
DEBUG LTAC Evaluated term: proj2