Goal:
    G : t  HI : invariants
  ============================
   ((exists l : labelling, correct_labelling l) -> acyclic_no_loop)


DEBUG:Going to execute:
intros [l Hl]; eapply acyclic_labelling
DEBUG LTAC Evaluated term: lsp_correctness