Include ecEq in cryptol_ss

[RyanGlScott]

Fixes #1347.

[RyanGlScott]

Well darn, this wasn't as simple of a fix as I had hoped. This ends up breaking the ecdsa test case:

  test_ecdsa:  

<elided>

[13:42:53.757] Proof succeeded! ec_full_add
[13:42:53.757] Time: 2.288272162s

[13:42:53.795] Proving rewrite rule:
[13:42:54.086] Stack trace:
"addsimps" (/home/runner/work/saw-script/saw-script/intTests/test_ecdsa/tmp/ecdsa.saw:1406:22-1406:30):
addsimp: theorem not an equation

FAIL (116.56s)
    intTests/IntegrationTest.hs:170:
    expected: ExitFailure 2
     but got: ExitSuccess

[brianhuffman]

If you uncomment the print_term t' line in the proof of the rewrite rule p384_ec_full_sub_simp, you can see the form of the theorem that is proved here:

[23:12:38.658] Proving rewrite rule:
[23:12:38.658] let { x@1 = Vec 384 Bool
      x@2 = x@1 * x@1
      x@3 = bvEq 384
    }
 in \(s : (x@1 * x@2)) ->
      \(t : x@2) ->
        pairEq x@1 x@2 x@3 (pairEq x@1 x@1 x@3 x@3)
          (p384_ec_full_sub (s,t))
          (p384_ec_full_add (s,t.1,p384_field_neg t.2))

So the problem is that the top-level connective is pairEq, which the saw-core library function ruleOfProp doesn't recognize as an equality relation. We probably need to fix #1261 before including ecEq in the simpset.