KnownTruth.findKnownTruth must relabel if needed

[wwitzel]

trafficstars

Because expressions are considered equal if they only differ by "alpha conversions" (a change of parameter variables of internal Lambda expressions), 'findKnownTruth' may return a KnownTruth with different labeling than what was requested. We should do the relabeling so it matches what is requested. Otherwise, we end up with surprised. This is from an e-mail on 5/22/2020 entitled "weird results understood" describing an encounter with this issue:

" At least, some of it is understood. The most disturbing was starting with {\forall_z \forall_b \forall_c \forall_d P(z, b, c, d)} |- \forall_z \forall_b \forall_c \forall_d P(z, b, c, d)

instantiating z:x and z:c and ending up with {\forall_z \forall_b \forall_c \forall_d P(a, b, c, d)} |- \forall_z \forall_b \forall_c \forall_d P(a, b, x, d)

Basically, the issue has to do with the fact that it regards \forall_z \forall_b \forall_c \forall_d P(z, b, c, d) as the same as \forall_a \forall_b \forall_c \forall_d P(a, b, c, d)

That's fine, but when it is looking for a known truth of \forall_z \forall_b \forall_c \forall_d P(z, b, c, d) it found the one for \forall_a \forall_b \forall_c \forall_d P(a, b, c, d) (since that had been proven before, by assumption) and went ahead and used that. So even though we thought we were instantiating the version with 'z', we were really instantiating the version with 'a' instead.

I don't think it was proving anything that is incorrect, but it is confusing, undesirable behavior that I need to fix. Thanks, Hoss, for asking questions that revealed this issue. It's better to find it now than later. "