Goal:
    G : t  l : labelling  Gl := relabel G l : t
  ============================
   (forall (x y : V.t) (n : Z),
    lsp Gl x y = Some n -> n = Z.of_nat (l y) - Z.of_nat (l x))


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2