Goal:
  
  G : t
  HI : invariants
  HG : acyclic_no_loop
  x : V.t
  n : Z
  y : V.t
  He : EdgeSet.In (x, n, y) (E G)
  xl : Z
  eq : lsp (s G) x = Some xl
  pos : 0 <= xl
  ============================
   (VSet.In y (V G))


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