- add various functions: boolToEither, equalString, bvSShiftR
- add BVVec type and associated functions
- for the above, add helper functions bvNat_bvToNat_id, genWithProof
- add datatype for iso-recursive types (IRT) and associated types/functions
- for the above, add ListSort and associated functions, uncurrySigma
- tweaks to CompM definitions

- GaloisInc/saw-core@59e6108 move prod destructing to after prove_refinement_eauto
- GaloisInc/saw-core@6028a21 remove bitvector type synonym from Prelude (needs latest heapster-saw)
- GaloisInc/saw-core@bf6cd78 remove EqP, replace with Eq (needs latest heapster-saw)
- GaloisInc/saw-core@a2d632c composeM is no longer skipped by the Coq translator
- GaloisInc/saw-core@9fa8e4f add IRT_BVVec, add gen_at_BVVec for IRT isomorphism
- GaloisInc/saw-core@7e098d5 prove foldIRT/unfoldIRT isomorphism
- GaloisInc/saw-core@0e53c87 use `match`es for IntroArg rules, clean up proofs
- GaloisInc/saw-core@fcb8625 more tweaks to proof automation
- GaloisInc/saw-core@7ac5115 move bv hints to SAWCoreBitvectors
- GaloisInc/saw-core@59bc79a performance improvements to prove_refinement...
- GaloisInc/saw-core@1fa5049 add `refines` and basic properties, more clean up, some partial progress
- GaloisInc/saw-core@f0ed599 Adds bvShl and enables CryptolPrimitivesForSAWCore to build