Goal:
    G : t  HI : invariants G  HG : acyclic_no_loop G  z : Z
  ============================
   (let H := CoreTactics.block in
    sweight (spath_refl G (V G) (s G)) = z ->
    ~ VSet.In (s G) (V G) -> let H0 := CoreTactics.block in z = 0)


DEBUG:Going to execute:
change T; CoreTactics.intros_until_block
Level 3: T
 has value 
(sweight (spath_refl G (V G) (s G)) = z ->
 ~ VSet.In (s G) (V G) -> let H := CoreTactics.block in z = 0)