Goal:
    G : t  HI : invariants G  HG : acyclic_no_loop G  n : Z  x : V.t  y : V.t
  ============================
   ((Some n <= lsp G x y)%nbar <->
    (if is_left (le_dec (Some n) (lsp G x y)) then true else false))


DEBUG:Going to execute:
destruct (le_dec (Some n) (lsp G x y)); cbn
DEBUG LTAC Evaluated term: leqb_vertices
DEBUG LTAC Evaluated term: leqb_vertices
DEBUG LTAC Evaluated term: lsp_optim
DEBUG LTAC Evaluated term: lsp_optim
DEBUG LTAC Evaluated term: lsp_optim
DEBUG LTAC Evaluated term: lsp_optim
DEBUG LTAC Evaluated term: (VSet.mem y (V G))