Failures in proof backends with latest Cryptol translation

[atomb]

Several of the integration tests are now failing during attempts to type-check SAWCore terms or complete proofs, with errors that seem related to the recent changes in the Cryptol to SAWCore translation.

For example:

Loading module Cryptol
Loading file "intTests/test0002/test.saw"
Loading module Main
ref type
let { x0 = Prelude.Vec 16 (Prelude.Vec 8 Prelude.Bool);
    }
 in (msg :: x0)
-> x0

saw: user error ("check_term" (intTests/test0002/test.saw:10:4):
Function argument type
  let { x0 = sort 0;
    }
 in #(x0,x0,x0)
doesn't match expected type
  sort 0