Goal:
    G : t  HI : invariants  HG : acyclic_no_loop
  ============================
   (forall e : EdgeSet.elt,
    EdgeSet.In e (E G) ->
    Z.of_nat (to_label (lsp (s G) e..s)) + e..w <=
    Z.of_nat (to_label (lsp (s G) e..t)))


DEBUG:Going to execute:
intros [[x n] y] He