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