Goal:
  
  G : t
  HI : invariants
  H : VSet.For_all (fun x : VSet.elt => lsp x x = Some 0) (V G)
  ============================
   acyclic_no_loop'


DEBUG:Going to execute:
eapply lsp_xx_acyclic
DEBUG LTAC Evaluated term: acyclic_lsp0_xx
DEBUG LTAC Evaluated term: acyclic_no_loop_loop'