Fix up comparisons with disperate variable sets
When a theory doesn't mention all of the variables, then counting, comparing, etc all become incorrect. Ultimately, a fix will need to come in the form of an NNF potentially storing a superset of the variables currently mentioned in descendants via the walk functionality.
This assumption should go away once this issue is resolved.
I gave this some thought during initial development but didn't come up with anything that really felt right.
One fix could be to add an optional keyword argument names for passing an explicit set of variables.
Comparing using the current behavior of .equivalent() is resistant to this problem, at least.
Ya, I considered the names argument too. Problem there is that it proliferates -- many places might need it (or have sub-procedures that need it). The make_smooth operation is certainly one that would require it...