While working with some automatically generated proofs I found that top-level disjoint variable restrictions seem to apply also before the $d statement.

In this example metamath-knife --verify complains "Distinct variable violation" on R-id, as if the $d x y $. at the end of the file was active for R-any.

$c term |- R $.
$v x y $.
x-term $f term x $.
y-term $f term y $.

R-any $a |- x R y $.
R-id $p |- x R x $= x-term x-term R-any $.

$( The offending $d may come after multiple declarations $)
$v z $.
z-term $f term z $.
padding-lemma $a |- x R x $.

$d x y $.

metamath-exe accepts the proof. Within a block metamath-knife also respects ordering, after adding ${ before R-any and $} after the $d this example metamath-knife --verify accepts the file.