Implement simultaneous substitution
Implement simultaneous substitution

Previously, the substitution works by performing one substitution at a
time until no more left-hand side can be matched.  This causes infinite
loop when we have the pattern on the left-hand side reappears on the
right-hand side.  By allowing a new option, we can have specially
decorate the left-hand side so that they can be substituted only when
they are from the original expression.

tschijnmo/drudge,tschijnmo/drudge,tschijnmo/drudge