Goal:
    G : t  HI : invariants  HG : acyclic_no_loop
  ============================
   (correct_labelling (fun x : V.t => to_label (lsp (s G) x)))


DEBUG:Going to execute:
split