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


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>