Goal:
    G : t  s0 : VSet.t  u : VSet.elt
  ============================
   (sweight (split (spath_refl s0 u) u (right eq_refl)).1 +
    sweight (split (spath_refl s0 u) u (right eq_refl)).2 =
    sweight (spath_refl s0 u))


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