NogDog Ah; your mention of "hope" made me think you had something against it.
For fun and the record, here's the method where I hit the snag, with the workaround included, just to give an idea of what things would start to look like without the
public function ConjunctionVisit(Conjunction $expr)
// Look for substitutions to Conjunction-bound variables. If this happens (it shouldn't, but at present
// there's nothing to stop it), we first replace the Conjunction's colliding bound variables with
// newly-minted ones, then update its expression to use the newly-minted variables in place of
// the existing ones. Then we can apply the substitutions we were actually passed.
$new_substitutions = ;
foreach($this->substitutions as [$var,])
if(in_array($var, $expr->variables, true))
$new_substitutions = [$var, LVariable()];
// No substitutions of bound variables. Business as usual, then.
$expression = $expr->expression->accept($this);
return ($expression === $expr->expression) ? $expr : Conjunction($expression, $expr->variables);
// If the number of new substitutions is 1 then array_map(null, ...) breaks down
// (this is known but undocumented behaviour: array_map(null, array) is a no-op)
if(count($new_substitutions) == 1)
$existing_variables = [$new_substitutions];
$new_variables = [$new_substitutions];
[$existing_variables, $new_variables] = array_map(null, ...$new_substitutions);
$new_variables = array_map(function($var)use($existing_variables, $new_variables)
$i = array_search($var, $existing_variables, true);
return ($i !== false) ? $new_variables[$i] : $var;
return Conjunction($expr->expression->accept(Substituting(...$new_substitutions, ...$this->substitutions)), $new_variables);