Support pair equality in rewriter.

[andreistefanescu]

No description provided.

[RyanGlScott]

Can you also add a test case for this? I'm thinking something like:

t <- prove_core z3 "(x : Vec 32 Bool) -> (y : Vec 32 Bool) -> EqTrue (pairEq (Vec 32 Bool) (Vec 32 Bool) (bvEq 32) (bvEq 32) (x, y) (x, y))";
print_term (rewrite (addsimp t empty_ss) {{ (27 : [8], 42 : [8]) }});

This currently fails on master:

$ ./bin/saw foo.saw 
[14:37:00.569] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/foo.saw"
[14:37:00.578] Stack trace:
"addsimp" (/home/ryanscott/Documents/Hacking/Haskell/saw-script/foo.saw:2:22-2:29)
addsimp: theorem not an equation

But I believe it would work after this PR.

[kquick]

Looks good; happy to approve once you've had a chance to add a test.