Goal:
    G : t  HG : acyclic_no_loop  x : V.t
  ============================
   (weight (pathOf_refl x) <= sweight (simplify2 (pathOf_refl x)))


DEBUG:Going to execute:
reflexivity
DEBUG LTAC Evaluated term: p