Improve counter-example printouts

[jldodds]

Record names from cryptol are lost in SAW counterexamples, making it very hard to debug. For example:

prove: 1 unsolved subgoal(s)
 [_ = (34, False, 1, 0, (0, 1, 0), False, False, 1, False, False), 
  _ = (False, 1, False, False, 1, False)]

[brianhuffman]

The problem is a combination of two things: First, saw-core encodes cryptol records as tuples, and does not preserve record field names; the field names are only preserved in the cryptol type associated with the saw-core term. Second, the cryptol types are not included in the saw-core ProofGoal type, so the proof tactics that generate the counterexamples do not have the information they need to reconstruct the record field names.

To fix the problem, we will need to extend the ProofGoal type to include the cryptol types of all quantified variables. However, this is not enough: We also need a way to discover the cryptol type of any fresh_symbolic variable that may occur within the predicate. In order to do this, we will probably need to add a lookup table to the TopLevel monad to track the cryptol types of all fresh_symbolic variables.

[sauclovian-g]

This is largely the same as #2119.