Avoid substituting to proxy symbols
split_vc, it is not rare to substitute variables to a proxy symbol:
H : r = (o [@mlw_proxy_symbol]) Goal : r + r = 5
split_vc would become:
Goal: o + o = 5
I think it is better to do the substitution from the other side.