Hi Dan,
here's a fragment of a proof. Applying the uspec/espec rule to line
94, I get the warning: "x will depend on: x1, x2, y1, y2."

Note that none of these variables occur inside the "source" I
generalized; nor occurs x inside the block where x1..., y2 occur.

It's not too bad, I just wanted to tell you :-).

Regards,

Thomas


[Non-text portions of this message have been removed]