[BUG] Replacing Variables laws bug

[Bram28]

Description

Replacing Bound variables (equivalence -> Quantifiers) law checks out when it shouldn't and vice versa

Steps to Reproduce

This should check out! .. the fact that the x's being replaced by y's occurs inside another x quantifier should not matter

And this one:

does check, but it should not: replacing the x from the universal quantifier Ax with a y to Ay means we should change any x inside the scope of that quantifier to a y as well, i.e. P(x) should change to P(y)

Expected Behavior

see above

Screenshots

No response

Additional Context

No response