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


DEBUG:Going to execute:
match goal with
           | |- let _ := CoreTactics.block in _ => intros _
           | |- _ => try (intro; CoreTactics.intros_until_block)
           end