Coalescing has issues with abstracting bound variables

[muenchnerkindl]

The PM employs coalescing for separating predicate-logic and temporal-logic reasoning. In particular, abstractions for predicate logic formulas are introduced on the fly when PTL is invoked so that the input that is sent to PTL is a formula of propositional temporal logic. However, that abstraction is fragile in the presence of bound variables. The following is a MWE.

CONSTANT S
VARIABLE x
A(m,n) == TRUE

THEOREM [](\A m,n \in S : WF_x(A(m,n))) => \A u,v \in S : WF_x(A(u,v))
BY PTL    \* fails

Renaming the bound variables on the right-hand side does not change the outcome.
Curiously, the following variant works even when the definition of Fair is not hidden.

THEOREM [](\A m,n \in S : WF_x(A(m,n))) => \A u,v \in S : WF_x(A(u,v))
<1>. DEFINE Fair == \A m,n \in S : WF_x(A(m,n))
<1>1. []Fair => Fair
  BY PTL
<1>. QED
  BY <1>1

This issue may be related to #120.