Goal:
    G : t  HI : invariants  HG : acyclic_no_loop  s : VSet.t  x : V.t
  ============================
   (lsp0 s x x = Some 0)


DEBUG:Going to execute:
pose proof (lsp0_spec_le (spath_refl s x)) as H