Modeling the notion of fresh variable into Metamath

[amelieled]

In the file theory/matching-logic.mm, someone can read:

${
    $d xX ph0 $.
    fresh-disjoint $a #Fresh xX ph0 $.
$}

So $d xX ph0 $. implies $a #Fresh xX ph0 $., that is $a #Fresh xX ph0 $. is weaker than $d xX ph0 $..
Do you think is it possible to replace everywhere (except in the four previous lines), $d A B $. by $a #Fresh A B $. ?

[zhengyao-lin]

In general, $d x y z ... $. has a different meaning that when the lemma is used, we need to instantiate terms with disjoint metavariables for metavariables x, y, and z (e.g. { x |-> ( \not y ), y |-> z, z |-> ( \not x ) } is a valid instantiation, but { x |-> ( \not y ), y |-> y, z |-> ( \not y ) } is not since z and x are both assigned terms with metavariable y), so in some scenarios it's not doable. But in cases when we need to assert that x appears free in ph0, we should indeed use #Fresh x ph0.

[amelieled]

But in cases when we need to assert that x appears free in ph0, we should indeed use #Fresh x ph0.

I have the feeling that it's always the case! But I'm not sure because I don't understand all the details.

For instance, do you think is it possible to change:

${
    $d xX ph0 $.
    positive-disjoint $a #Positive xX ph0 $.
$}
[...]
${
    $d xX ph0 $.
    negative-disjoint $a #Negative xX ph0 $.
$}

by

${
    hyp-fresh $e #Fresh xX ph0 $.
    positive-disjoint $a #Positive xX ph0 $.
$}
[...]
${
    hyp-fresh $e #Fresh xX ph0 $.
    negative-disjoint $a #Negative xX ph0 $.
$}

?
I think it's a very important task to transform all $d ... declarations by $e #Fresh ... hypothesis, when it's possible!

Moreover, why

positive-in-var $a #Positive xX yY $.

is different from:

${
    $d xX yY $.
    negative-in-var $a #Negative xX yY $.
$}

i.e. $d xX yY doesn't appear in the #Positive case?