Goal:
    G : t  H : invariants G  x : V.t  y : V.t  e : EdgeOf G x y
  ============================
   (Some e.π1 <= lsp G x y)%nbar


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