SAWCore fixes for variable name shadowing

[brianhuffman]

This PR fixes a few different SAWCore functions so that they work correctly on terms that have variable name shadowing.

• scMatch
• scmConvertible
• alphaEquiv

Fixes #2939. Fixes #2954.

Currently marked as draft until I replace [VarName] with a more efficient data structure for representing bound variable contexts.

[brianhuffman]

I located the problem with the ECDSA proof. In the ec_mul_ov subproof, after proving the first proof obligation, the Haskell evidence-checking function convertibleProps calls scConvertible on a pair of very large terms taken from the proof goal. (How big? See #2965.)

saw-script/saw-central/src/SAWCentral/Proof.hs

Lines 619 to 625 in 6ab55c1

	convertibleProps :: SharedContext -> [Prop] -> [Prop] -> IO Bool
	convertibleProps _sc [] [] = return True
	convertibleProps sc (p1:ps1) (p2:ps2) =
	do ok1 <- scConvertible sc True (unProp p1) (unProp p2)
	ok2 <- convertibleProps sc ps1 ps2
	return (ok1 && ok2)
	convertibleProps _sc _ _ = return False

Function scConvertible has a "succeed early" case that returns True immediately if the two terms are the same.

saw-script/saw-central/src/SAWCentral/Proof.hs

Lines 619 to 625 in 6ab55c1

	convertibleProps :: SharedContext -> [Prop] -> [Prop] -> IO Bool
	convertibleProps _sc [] [] = return True
	convertibleProps sc (p1:ps1) (p2:ps2) =
	do ok1 <- scConvertible sc True (unProp p1) (unProp p2)
	ok2 <- convertibleProps sc ps1 ps2
	return (ok1 && ok2)
	convertibleProps _sc _ _ = return False

However, this PR made this short-cut case a bit more conservative in the presence of free variables, forcing scConvertible to traverse the terms instead down to the point where it was comparing closed subterms. The real problem is that scConvertible does not take advantage of observable sharing, and the fully-expanded terms are so astronomically large that the term traversal will never finish in practice.

The quick fix is to strengthen the shortcut case so that it applies at least as often as it used to. However, this is really quite fragile: A mismatch in bound variable names somewhere would cause the super-exponential runtime again. The better fix is to make scConvertible use observable sharing to fix the useless slow code path.