diff --git a/saw/Cryptol.sawcore b/saw/Cryptol.sawcore
index a177e28..624cc84 100644
--- a/saw/Cryptol.sawcore
+++ b/saw/Cryptol.sawcore
@@ -117,66 +117,6 @@ seqConst :: (n :: Num) -> (a :: sort 0) -> a -> seq n a;
 seqConst (TCNum n) = replicate n;
 seqConst TCInf = streamConst;
 
---------------------------------------------------------------------------------
--- Types
-
-data KType :: sort 0 where {
-    TCBit :: KType;
-    TCSeq :: Num -> KType -> KType;
-    TCFun :: KType -> KType -> KType;
-    TCUnit :: KType;
-    TCPair :: KType -> KType -> KType;
-    TCEmpty :: KType;
-    TCField :: String -> KType -> KType -> KType;
-  }
-
-ty :: KType -> sort 0;
-ty TCBit = Bool;
-ty (TCSeq n a) = seq n (ty a);
-ty (TCFun a b) = ty a -> ty b;
-ty TCUnit = #();
-ty (TCPair a b) = #(ty a | ty b);
-ty TCEmpty = #{};
-ty (TCField s a b) = #{ (s) :: ty a | ty b };
-
---------------------------------------------------------------------------------
--- Predicate symbols
-
--- Partial functions to select instances (terms translated from
--- type-correct Cryptol should never hit the undefined cases)
-
-ePArith :: (a :: KType) -> PArith a;
---ePArith TCBit = undefined;
---ePArith (TCSeq TCInf TCBit) = undefined;
-ePArith (TCSeq n TCBit) = PArithWord n;
-ePArith (TCSeq n (TCSeq m a)) = PArithSeq n (TCSeq m a) (ePArith (TCSeq m a));
-ePArith (TCSeq n (TCFun a b)) = PArithSeq n (TCFun a b) (ePArith (TCFun a b));
-ePArith (TCSeq n TCUnit) = PArithSeq n TCUnit (ePArith TCUnit);
-ePArith (TCSeq n (TCPair a b)) = PArithSeq n (TCPair a b) (ePArith (TCPair a b));
-ePArith (TCSeq n TCEmpty) = PArithSeq n TCEmpty (ePArith TCEmpty);
-ePArith (TCSeq n (TCField s a b)) = PArithSeq n (TCField s a b) (ePArith (TCField s a b));
-ePArith (TCFun a b) = PArithFun a b (ePArith b);
-ePArith TCUnit = PArithUnit;
-ePArith (TCPair a b) = PArithPair a b (ePArith a) (ePArith b);
-ePArith TCEmpty = PArithEmpty;
-ePArith (TCField s a b) = PArithField s a b (ePArith a) (ePArith b);
-
-ePCmp :: (a :: KType) -> PCmp a;
---ePCmp (TCSeq TCInf a) = undefined;
-ePCmp (TCSeq n TCBit) = PCmpWord n;
-ePCmp (TCSeq n (TCSeq m a)) = PCmpSeq n (TCSeq m a) (ePCmp (TCSeq m a));
---ePCmp (TCSeq (TCNum n) (TCFun a b)) = PCmpSeq n (TCFun a b) (ePCmp (TCFun a b));
-ePCmp (TCSeq n TCUnit) = PCmpSeq n TCUnit (ePCmp TCUnit);
-ePCmp (TCSeq n (TCPair a b)) = PCmpSeq n (TCPair a b) (ePCmp (TCPair a b));
-ePCmp (TCSeq n TCEmpty) = PCmpSeq n TCEmpty (ePCmp TCEmpty);
-ePCmp (TCSeq n (TCField s a b)) = PCmpSeq n (TCField s a b) (ePCmp (TCField s a b));
-ePCmp TCBit = PCmpBit;
---ePCmp (TCFun a b) = undefined;
-ePCmp TCUnit = PCmpUnit;
-ePCmp (TCPair a b) = PCmpPair a b (ePCmp a) (ePCmp b);
-ePCmp TCEmpty = PCmpEmpty;
-ePCmp (TCField s a b) = PCmpField s a b (ePCmp a) (ePCmp b);
-
 --------------------------------------------------------------------------------
 -- Auxiliary functions
 
@@ -241,7 +181,7 @@ seqZip a b TCInf (TCNum n) xs ys = gen n #(a, b) (\(i :: Nat) -> (streamGet a xs
 seqZip a b TCInf TCInf xs ys = streamMap2 a b #(a, b) (\(x::a) -> \(y::b) -> (x, y)) xs ys;
 
 --------------------------------------------------------------------------------
--- Arith functions
+-- Arith and Logic functions
 
 seqBinary :: (n :: Num) -> (a :: sort 0) -> (a -> a -> a) -> seq n a -> seq n a -> seq n a;
 seqBinary (TCNum n) a f = zipWith a a a f n;
@@ -277,21 +217,129 @@ fieldBinary s a b f g { (_) = x1 | x2 } { (_) = y1 | y2 } = { (s) = f x1 y1 | g
 funBinary :: (a b :: sort 0) -> (b -> b -> b) -> (a -> b) -> (a -> b) -> (a -> b);
 funBinary a b op f g x = op (f x) (g x);
 
-PArith :: KType -> sort 0;
-PArith a =
-  #{ add :: ty a -> ty a -> ty a
-   , sub :: ty a -> ty a -> ty a
-   , mul :: ty a -> ty a -> ty a
-   , div :: ty a -> ty a -> ty a
-   , mod :: ty a -> ty a -> ty a
-   , exp :: ty a -> ty a -> ty a
-   , lg2 :: ty a -> ty a
-   , neg :: ty a -> ty a
+errorUnary :: (a :: sort 0) -> a -> a;
+errorUnary a _ = error a "invalid class instance";
+
+errorBinary :: (a :: sort 0) -> a -> a -> a;
+errorBinary a _ _ = error a "invalid class instance";
+
+--------------------------------------------------------------------------------
+-- Comparisons
+
+boolCmp :: Bool -> Bool -> Bool -> Bool;
+boolCmp x y k = ite Bool x (and y k) (or y k);
+
+bvCmp :: (n :: Nat) -> bitvector n -> bitvector n -> Bool -> Bool;
+bvCmp n x y k = or (bvult n x y) (and (bvEq n x y) k);
+
+vecCmp :: (n :: Nat) -> (a :: sort 0) -> (a -> a -> Bool -> Bool)
+       -> (Vec n a -> Vec n a -> Bool -> Bool);
+vecCmp n a f xs ys k =
+  foldr (Bool -> Bool) Bool n (\(f :: Bool -> Bool) -> f) k
+    (zipWith a a (Bool -> Bool) f n xs ys);
+
+unitCmp :: #() -> #() -> Bool -> Bool;
+unitCmp _ _ _ = False;
+
+emptyCmp :: #{} -> #{} -> Bool -> Bool;
+emptyCmp _ _ _ = False;
+
+pairCmp :: (a b :: sort 0) -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool -> Bool)
+        -> #(a | b) -> #(a | b) -> Bool -> Bool;
+pairCmp a b f g (x1 | x2) (y1 | y2) k = f x1 y1 (g x2 y2 k);
+
+fieldCmp :: (s :: String) -> (a b :: sort 0)
+         -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool -> Bool)
+         -> #{ (s) :: a | b } -> #{ (s) :: a | b } -> Bool -> Bool;
+fieldCmp s a b f g { (_) = x1 | x2 } { (_) = y1 | y2 } k = f x1 y1 (g x2 y2 k);
+
+errorCmp :: (a :: sort 0) -> a -> a -> Bool -> Bool;
+errorCmp _ _ _ _ = error Bool "invalid Cmp instance";
+
+--------------------------------------------------------------------------------
+-- Dictionaries and overloading
+
+Dict :: sort 0 -> sort 0;
+Dict a =
+  #{ and  :: a -> a -> a
+   , or   :: a -> a -> a
+   , xor  :: a -> a -> a
+   , not  :: a -> a
+   , zero :: a
+   , cmp  :: a -> a -> Bool -> Bool
+   , add  :: a -> a -> a
+   , sub  :: a -> a -> a
+   , mul  :: a -> a -> a
+   , div  :: a -> a -> a
+   , mod  :: a -> a -> a
+   , exp  :: a -> a -> a
+   , lg2  :: a -> a
+   , neg  :: a -> a
    };
 
-PArithWord :: (n :: Num) -> PArith (TCSeq n TCBit);
-PArithWord (TCNum n) =
-  { add = bvAdd n
+DictBit :: Dict Bool;
+DictBit =
+  { and  = and
+  , or   = or
+  , xor  = xor
+  , not  = not
+  , zero = False
+  , cmp  = boolCmp
+  , add = errorBinary Bool
+  , sub = errorBinary Bool
+  , mul = errorBinary Bool
+  , div = errorBinary Bool
+  , mod = errorBinary Bool
+  , exp = errorBinary Bool
+  , lg2 = errorUnary Bool
+  , neg = errorUnary Bool
+  };
+
+DictVec :: (a :: sort 0) -> Dict a -> (n :: Nat) -> Dict (Vec n a);
+DictVec a pa n =
+  { and  = zipWith a a a pa.and n
+  , or   = zipWith a a a pa.or  n
+  , xor  = zipWith a a a pa.xor n
+  , not  = map a a pa.not n
+  , zero = replicate n a pa.zero
+  , cmp  = vecCmp n a pa.cmp
+  , add = zipWith a a a pa.add n
+  , sub = zipWith a a a pa.sub n
+  , mul = zipWith a a a pa.mul n
+  , div = zipWith a a a pa.div n
+  , mod = zipWith a a a pa.mod n
+  , exp = zipWith a a a pa.exp n
+  , lg2 = map a a pa.lg2 n
+  , neg = map a a pa.neg n
+  };
+
+DictStream :: (a :: sort 0) -> Dict a -> Dict (Stream a);
+DictStream a pa =
+  { and  = streamMap2 a a a pa.and
+  , or   = streamMap2 a a a pa.or
+  , xor  = streamMap2 a a a pa.xor
+  , not  = streamMap a a pa.not
+  , zero = streamConst a pa.zero
+  , cmp  = errorCmp (Stream a)
+  , add = streamMap2 a a a pa.add
+  , sub = streamMap2 a a a pa.sub
+  , mul = streamMap2 a a a pa.mul
+  , div = streamMap2 a a a pa.div
+  , mod = streamMap2 a a a pa.mod
+  , exp = streamMap2 a a a pa.exp
+  , lg2 = streamMap a a pa.lg2
+  , neg = streamMap a a pa.neg
+  };
+
+DictWord :: (n :: Nat) -> Dict (Vec n Bool);
+DictWord n =
+  { and  = bvAnd n
+  , or   = bvOr  n
+  , xor  = bvXor n
+  , not  = bvNot n
+  , zero = bvNat n 0
+  , cmp  = bvCmp n
+  , add = bvAdd n
   , sub = bvSub n
   , mul = bvMul n
   , div = bvUDiv n
@@ -301,33 +349,33 @@ PArithWord (TCNum n) =
   , neg = bvNeg n
   };
 
-PArithSeq :: (n :: Num) -> (a :: KType) -> PArith a -> PArith (TCSeq n a);
-PArithSeq n a pa =
-  { add = seqBinary n (ty a) pa.add
-  , sub = seqBinary n (ty a) pa.sub
-  , mul = seqBinary n (ty a) pa.mul
-  , div = seqBinary n (ty a) pa.div
-  , mod = seqBinary n (ty a) pa.mod
-  , exp = seqBinary n (ty a) pa.exp
-  , lg2 = seqMap (ty a) (ty a) n pa.lg2
-  , neg = seqMap (ty a) (ty a) n pa.neg
-  };
-
-PArithFun :: (a b :: KType) -> PArith b -> PArith (TCFun a b);
-PArithFun a b pb =
-  { add = funBinary (ty a) (ty b) pb.add
-  , sub = funBinary (ty a) (ty b) pb.sub
-  , mul = funBinary (ty a) (ty b) pb.mul
-  , div = funBinary (ty a) (ty b) pb.div
-  , mod = funBinary (ty a) (ty b) pb.mod
-  , exp = funBinary (ty a) (ty b) pb.exp
-  , lg2 = compose (ty a) (ty b) (ty b) pb.lg2
-  , neg = compose (ty a) (ty b) (ty b) pb.neg
+DictFun :: (a b :: sort 0) -> Dict b -> Dict (a -> b);
+DictFun a b pb =
+  { and  = funBinary a b pb.and
+  , or   = funBinary a b pb.or
+  , xor  = funBinary a b pb.xor
+  , not  = compose a b b pb.not
+  , zero = (\(_ :: a) -> pb.zero)
+  , cmp  = errorCmp (a -> b)
+  , add = funBinary a b pb.add
+  , sub = funBinary a b pb.sub
+  , mul = funBinary a b pb.mul
+  , div = funBinary a b pb.div
+  , mod = funBinary a b pb.mod
+  , exp = funBinary a b pb.exp
+  , lg2 = compose a b b pb.lg2
+  , neg = compose a b b pb.neg
   };
 
-PArithUnit :: PArith TCUnit;
-PArithUnit =
-  { add = unitBinary
+DictUnit :: Dict #();
+DictUnit =
+  { and  = unitBinary
+  , or   = unitBinary
+  , xor  = unitBinary
+  , not  = unitUnary
+  , zero = ()
+  , cmp  = unitCmp
+  , add = unitBinary
   , sub = unitBinary
   , mul = unitBinary
   , div = unitBinary
@@ -337,21 +385,33 @@ PArithUnit =
   , neg = unitUnary
   };
 
-PArithPair :: (a b :: KType) -> PArith a -> PArith b -> PArith (TCPair a b);
-PArithPair a b pa pb =
-  { add = pairBinary (ty a) (ty b) pa.add pb.add
-  , sub = pairBinary (ty a) (ty b) pa.sub pb.sub
-  , mul = pairBinary (ty a) (ty b) pa.mul pb.mul
-  , div = pairBinary (ty a) (ty b) pa.div pb.div
-  , mod = pairBinary (ty a) (ty b) pa.mod pb.mod
-  , exp = pairBinary (ty a) (ty b) pa.exp pb.exp
-  , lg2 = pairUnary (ty a) (ty b) pa.lg2 pb.lg2
-  , neg = pairUnary (ty a) (ty b) pa.neg pb.neg
+DictPair :: (a b :: sort 0) -> Dict a -> Dict b -> Dict #(a | b);
+DictPair a b pa pb =
+  { and  = pairBinary a b pa.and pb.and
+  , or   = pairBinary a b pa.or  pb.or
+  , xor  = pairBinary a b pa.xor pb.xor
+  , not  = pairUnary a b pa.not pb.not
+  , zero = (pa.zero | pb.zero)
+  , cmp  = pairCmp a b pa.cmp pb.cmp
+  , add = pairBinary a b pa.add pb.add
+  , sub = pairBinary a b pa.sub pb.sub
+  , mul = pairBinary a b pa.mul pb.mul
+  , div = pairBinary a b pa.div pb.div
+  , mod = pairBinary a b pa.mod pb.mod
+  , exp = pairBinary a b pa.exp pb.exp
+  , lg2 = pairUnary a b pa.lg2 pb.lg2
+  , neg = pairUnary a b pa.neg pb.neg
   };
 
-PArithEmpty :: PArith TCEmpty;
-PArithEmpty =
-  { add = emptyBinary
+DictEmpty :: Dict #{};
+DictEmpty =
+  { and  = emptyBinary
+  , or   = emptyBinary
+  , xor  = emptyBinary
+  , not  = emptyUnary
+  , zero = {}
+  , cmp  = emptyCmp
+  , add = emptyBinary
   , sub = emptyBinary
   , mul = emptyBinary
   , div = emptyBinary
@@ -361,95 +421,58 @@ PArithEmpty =
   , neg = emptyUnary
   };
 
-PArithField :: (s :: String) -> (a b :: KType) -> PArith a -> PArith b -> PArith (TCField s a b);
-PArithField s a b pa pb =
-  { add = fieldBinary s (ty a) (ty b) pa.add pb.add
-  , sub = fieldBinary s (ty a) (ty b) pa.sub pb.sub
-  , mul = fieldBinary s (ty a) (ty b) pa.mul pb.mul
-  , div = fieldBinary s (ty a) (ty b) pa.div pb.div
-  , mod = fieldBinary s (ty a) (ty b) pa.mod pb.mod
-  , exp = fieldBinary s (ty a) (ty b) pa.exp pb.exp
-  , lg2 = fieldUnary s (ty a) (ty b) pa.lg2 pb.lg2
-  , neg = fieldUnary s (ty a) (ty b) pa.neg pb.neg
+DictField :: (s :: String) -> (a b :: sort 0) -> Dict a -> Dict b -> Dict #{ (s) :: a | b };
+DictField s a b pa pb =
+  { and  = fieldBinary s a b pa.and pb.and
+  , or   = fieldBinary s a b pa.or  pb.or
+  , xor  = fieldBinary s a b pa.xor pb.xor
+  , not  = fieldUnary s a b pa.not pb.not
+  , zero = { (s) = pa.zero | pb.zero }
+  , cmp  = fieldCmp s a b pa.cmp pb.cmp
+  , add = fieldBinary s a b pa.add pb.add
+  , sub = fieldBinary s a b pa.sub pb.sub
+  , mul = fieldBinary s a b pa.mul pb.mul
+  , div = fieldBinary s a b pa.div pb.div
+  , mod = fieldBinary s a b pa.mod pb.mod
+  , exp = fieldBinary s a b pa.exp pb.exp
+  , lg2 = fieldUnary s a b pa.lg2 pb.lg2
+  , neg = fieldUnary s a b pa.neg pb.neg
   };
 
-logicBinary :: ((n :: Nat) -> bitvector n -> bitvector n -> bitvector n)
-            -> (Bool -> Bool -> Bool)
-            -> (a :: KType) -> ty a -> ty a -> ty a;
-logicBinary bvOp bitOp TCBit = bitOp;
-logicBinary bvOp bitOp (TCFun a b) = funBinary (ty a) (ty b) (logicBinary bvOp bitOp b);
-logicBinary bvOp bitOp TCUnit = unitBinary;
-logicBinary bvOp bitOp (TCPair a b) =
-  pairBinary (ty a) (ty b) (logicBinary bvOp bitOp a) (logicBinary bvOp bitOp b);
-logicBinary bvOp bitOp TCEmpty = emptyBinary;
-logicBinary bvOp bitOp (TCField s a b) =
-  fieldBinary s (ty a) (ty b) (logicBinary bvOp bitOp a) (logicBinary bvOp bitOp b);
-logicBinary bvOp bitOp (TCSeq (TCNum n) TCBit) = bvOp n;
-logicBinary bvOp bitOp (TCSeq TCInf TCBit) = streamMap2 Bool Bool Bool bitOp;
-logicBinary bvOp bitOp (TCSeq n (TCSeq m a)) =
-   seqBinary n (seq m (ty a)) (logicBinary bvOp bitOp (TCSeq m a));
-logicBinary bvOp bitOp (TCSeq n (TCFun a b)) =
-   seqBinary n (ty a -> ty b) (logicBinary bvOp bitOp (TCFun a b));
-logicBinary bvOp bitOp (TCSeq n TCUnit) = seqBinary n #() unitBinary;
-logicBinary bvOp bitOp (TCSeq n (TCPair a b)) =
-   seqBinary n #(ty a | ty b) (logicBinary bvOp bitOp (TCPair a b));
-logicBinary bvOp bitOp (TCSeq n TCEmpty) = seqBinary n #{} emptyBinary;
-logicBinary bvOp bitOp (TCSeq n (TCField s a b)) =
-   seqBinary n (ty (TCField s a b)) (logicBinary bvOp bitOp (TCField s a b));
+Ops :: sort 0 -> sort 0;
+Ops a = #{ this :: Dict a, vec :: (n :: Nat) -> Dict (Vec n a) };
 
---------------------------------------------------------------------------------
--- Comparisons
+OpsBit :: Ops Bool;
+OpsBit = { this = DictBit, vec = DictWord };
 
-boolCmp :: Bool -> Bool -> Bool -> Bool;
-boolCmp x y k = ite Bool x (and y k) (or y k);
+OpsSeq :: (n :: Num) -> (a :: sort 0) -> Ops a -> Ops (seq n a);
+OpsSeq (TCNum n) a pa =
+  { this = pa.vec n
+  , vec = DictVec (Vec n a) (pa.vec n) };
+OpsSeq TCInf a pa =
+  { this = DictStream a pa.this
+  , vec = DictVec (Stream a) (DictStream a pa.this) };
 
-bvCmp :: (n :: Nat) -> bitvector n -> bitvector n -> Bool -> Bool;
-bvCmp n x y k = or (bvult n x y) (and (bvEq n x y) k);
+OpsFun :: (a b :: sort 0) -> Ops b -> Ops (a -> b);
+OpsFun a b pb =
+  { this = DictFun a b pb.this
+  , vec = DictVec (a -> b) (DictFun a b pb.this) };
 
-vecCmp :: (n :: Nat) -> (a :: sort 0) -> (a -> a -> Bool -> Bool)
-       -> (Vec n a -> Vec n a -> Bool -> Bool);
-vecCmp n a f xs ys k =
-  foldr (Bool -> Bool) Bool n (\(f :: Bool -> Bool) -> f) k
-    (zipWith a a (Bool -> Bool) f n xs ys);
+OpsUnit :: Ops #();
+OpsUnit = { this = DictUnit, vec = DictVec #() DictUnit };
 
-unitCmp :: #() -> #() -> Bool -> Bool;
-unitCmp _ _ _ = False;
+OpsPair :: (a b :: sort 0) -> Ops a -> Ops b -> Ops #(a | b);
+OpsPair a b pa pb =
+  { this = DictPair a b pa.this pb.this
+  , vec = DictVec #(a | b) (DictPair a b pa.this pb.this) };
 
-emptyCmp :: #{} -> #{} -> Bool -> Bool;
-emptyCmp _ _ _ = False;
+OpsEmpty :: Ops #{};
+OpsEmpty = { this = DictEmpty, vec = DictVec #{} DictEmpty };
 
-pairCmp :: (a b :: sort 0) -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool -> Bool)
-        -> #(a | b) -> #(a | b) -> Bool -> Bool;
-pairCmp a b f g (x1 | x2) (y1 | y2) k = f x1 y1 (g x2 y2 k);
-
-fieldCmp :: (s :: String) -> (a b :: sort 0)
-         -> (a -> a -> Bool -> Bool) -> (b -> b -> Bool -> Bool)
-         -> #{ (s) :: a | b } -> #{ (s) :: a | b } -> Bool -> Bool;
-fieldCmp s a b f g { (_) = x1 | x2 } { (_) = y1 | y2 } k = f x1 y1 (g x2 y2 k);
-
-PCmp :: KType -> sort 0;
-PCmp a = #{ cmpLt :: ty a -> ty a -> Bool -> Bool };
-
-PCmpWord :: (n :: Num) -> PCmp (TCSeq n TCBit);
-PCmpWord (TCNum n) = { cmpLt = bvCmp n };
-
-PCmpBit :: PCmp TCBit;
-PCmpBit = { cmpLt = boolCmp };
-
-PCmpSeq :: (n :: Num) -> (a :: KType) -> PCmp a -> PCmp (TCSeq n a);
-PCmpSeq (TCNum n) a pa = { cmpLt = vecCmp n (ty a) pa.cmpLt };
-
-PCmpUnit :: PCmp TCUnit;
-PCmpUnit = { cmpLt = unitCmp };
-
-PCmpPair :: (a b :: KType) -> PCmp a -> PCmp b -> PCmp (TCPair a b);
-PCmpPair a b pa pb = { cmpLt = pairCmp (ty a) (ty b) pa.cmpLt pb.cmpLt };
-
-PCmpEmpty :: PCmp TCEmpty;
-PCmpEmpty = { cmpLt = emptyCmp };
-
-PCmpField :: (s :: String) -> (a b :: KType) -> PCmp a -> PCmp b -> PCmp (TCField s a b);
-PCmpField s a b pa pb = { cmpLt = fieldCmp s (ty a) (ty b) pa.cmpLt pb.cmpLt };
+OpsField :: (s :: String) -> (a b :: sort 0) -> Ops a -> Ops b -> Ops #{ (s) :: a | b };
+OpsField s a b pa pb =
+  { this = DictField s a b pa.this pb.this
+  , vec = DictVec #{ (s) :: a | b } (DictField s a b pa.this pb.this) };
 
 --------------------------------------------------------------------------------
 -- Primitive Cryptol functions
@@ -458,156 +481,130 @@ ecDemote :: (val bits :: Num) -> seq bits Bool;
 ecDemote (TCNum val) (TCNum bits) = bvNat bits val;
 
 -- Arith
-ecPlus :: (a :: KType) -> PArith a -> ty a -> ty a -> ty a;
-ecPlus a pa = pa.add;
+ecPlus :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecPlus a pa = pa.this.add;
 
-ecMinus :: (a :: KType) -> PArith a -> ty a -> ty a -> ty a;
-ecMinus a pa = pa.sub;
+ecMinus :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecMinus a pa = pa.this.sub;
 
-ecMul :: (a :: KType) -> PArith a -> ty a -> ty a -> ty a;
-ecMul a pa = pa.mul;
+ecMul :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecMul a pa = pa.this.mul;
 
-ecDiv :: (a :: KType) -> PArith a -> ty a -> ty a -> ty a;
-ecDiv a pa = pa.div;
+ecDiv :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecDiv a pa = pa.this.div;
 
-ecMod :: (a :: KType) -> PArith a -> ty a -> ty a -> ty a;
-ecMod a pa = pa.mod;
+ecMod :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecMod a pa = pa.this.mod;
 
-ecExp :: (a :: KType) -> PArith a -> ty a -> ty a -> ty a;
-ecExp a pa = pa.exp;
+ecExp :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecExp a pa = pa.this.exp;
 
-ecLg2 :: (a :: KType) -> PArith a -> ty a -> ty a;
-ecLg2 a pa = pa.lg2;
+ecLg2 :: (a :: sort 0) -> Ops a -> a -> a;
+ecLg2 a pa = pa.this.lg2;
 
-ecNeg :: (a :: KType) -> PArith a -> ty a -> ty a;
-ecNeg a pa = pa.neg;
+ecNeg :: (a :: sort 0) -> Ops a -> a -> a;
+ecNeg a pa = pa.this.neg;
 
 -- Cmp
-ecLt :: (a :: KType) -> PCmp a -> ty a -> ty a -> Bool;
-ecLt a pa x y = pa.cmpLt x y False;
+ecLt :: (a :: sort 0) -> Ops a -> a -> a -> Bool;
+ecLt a pa x y = pa.this.cmp x y False;
 
-ecGt :: (a :: KType) -> PCmp a -> ty a -> ty a -> Bool;
+ecGt :: (a :: sort 0) -> Ops a -> a -> a -> Bool;
 ecGt a pa x y = ecLt a pa y x;
 
-ecLtEq  :: (a :: KType) -> PCmp a -> ty a -> ty a -> Bool;
+ecLtEq  :: (a :: sort 0) -> Ops a -> a -> a -> Bool;
 ecLtEq a pa x y = not (ecLt a pa y x);
 
-ecGtEq  :: (a :: KType) -> PCmp a -> ty a -> ty a -> Bool;
+ecGtEq  :: (a :: sort 0) -> Ops a -> a -> a -> Bool;
 ecGtEq a pa x y = not (ecLt a pa x y);
 
-ecEq :: (a :: KType) -> PCmp a -> ty a -> ty a -> Bool;
-ecEq a _ = eq (ty a);
+ecEq :: (a :: sort 0) -> Ops a -> a -> a -> Bool;
+ecEq a _ = eq a;
 
-ecNotEq :: (a :: KType) -> PCmp a -> ty a -> ty a -> Bool;
+ecNotEq :: (a :: sort 0) -> Ops a -> a -> a -> Bool;
 ecNotEq a pa x y = not (ecEq a pa x y);
 
-ecFunEq :: (a b :: KType) -> PCmp b -> (ty a -> ty b) -> (ty a -> ty b) -> ty a -> Bool;
-ecFunEq a b pb f g x = ecEq b pb (f x) (g x);
+ecFunEq :: (a :: sort 0) -> Ops a -> (b :: sort 0) -> Ops b -> (a -> b) -> (a -> b) -> a -> Bool;
+ecFunEq a _ b pb f g x = ecEq b pb (f x) (g x);
 
-ecFunNotEq :: (a b :: KType) -> PCmp b -> (ty a -> ty b) -> (ty a -> ty b) -> ty a -> Bool;
-ecFunNotEq a b pb f g x = ecNotEq b pb (f x) (g x);
+ecFunNotEq :: (a :: sort 0) -> Ops a -> (b :: sort 0) -> Ops b -> (a -> b) -> (a -> b) -> a -> Bool;
+ecFunNotEq a _ b pb f g x = ecNotEq b pb (f x) (g x);
 
 -- Logic
 
-ecAnd :: (a :: KType) -> ty a -> ty a -> ty a;
-ecAnd = logicBinary bvAnd and;
-
-ecOr :: (a :: KType) -> ty a -> ty a -> ty a;
-ecOr = logicBinary bvOr or;
-
-ecXor :: (a :: KType) -> ty a -> ty a -> ty a;
-ecXor = logicBinary bvXor xor;
-
-ecCompl :: (a :: KType) -> ty a -> ty a;
-ecCompl TCBit = not;
-ecCompl (TCFun a b) = compose (ty a) (ty b) (ty b) (ecCompl b);
-ecCompl TCUnit = unitUnary;
-ecCompl (TCPair a b) = pairUnary (ty a) (ty b) (ecCompl a) (ecCompl b);
-ecCompl TCEmpty = emptyUnary;
-ecCompl (TCField s a b) = fieldUnary s (ty a) (ty b) (ecCompl a) (ecCompl b);
-ecCompl (TCSeq (TCNum n) TCBit) = bvNot n;
-ecCompl (TCSeq TCInf TCBit) = streamMap Bool Bool not;
-ecCompl (TCSeq n (TCSeq m a)) = seqMap (seq m (ty a)) (seq m (ty a)) n (ecCompl (TCSeq m a));
-ecCompl (TCSeq n (TCFun a b)) = seqMap (ty a -> ty b) (ty a -> ty b) n (ecCompl (TCFun a b));
-ecCompl (TCSeq n TCUnit) = seqMap #() #() n unitUnary;
-ecCompl (TCSeq n (TCPair a b)) = seqMap #(ty a | ty b) #(ty a | ty b) n (ecCompl (TCPair a b));
-ecCompl (TCSeq n TCEmpty) = seqMap #{} #{} n emptyUnary;
-ecCompl (TCSeq n (TCField s a b)) = seqMap (ty (TCField s a b)) (ty (TCField s a b)) n (ecCompl (TCField s a b));
-
-ecZero :: (a :: KType) -> ty a;
-ecZero TCBit = False;
-ecZero (TCFun a b) = (\(_::ty a) -> ecZero b);
-ecZero TCUnit = ();
-ecZero (TCPair a b) = (ecZero a | ecZero b);
-ecZero TCEmpty = {};
-ecZero (TCField s a b) = { (s) = ecZero a | ecZero b };
-ecZero (TCSeq (TCNum n) TCBit) = bvNat n 0;
-ecZero (TCSeq TCInf TCBit) = streamConst Bool False;
-ecZero (TCSeq n (TCSeq m a)) = seqConst n (seq m (ty a)) (ecZero (TCSeq m a));
-ecZero (TCSeq n (TCFun a b)) = seqConst n (ty a -> ty b) (ecZero (TCFun a b));
-ecZero (TCSeq n TCUnit) = seqConst n #() ();
-ecZero (TCSeq n (TCPair a b)) = seqConst n #(ty a | ty b) (ecZero (TCPair a b));
-ecZero (TCSeq n TCEmpty) = seqConst n #{} {};
-ecZero (TCSeq n (TCField s a b)) = seqConst n #{ (s) :: ty a | ty b } (ecZero (TCField s a b));
+ecAnd :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecAnd a pa = pa.this.and;
+
+ecOr :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecOr a pa = pa.this.or;
+
+ecXor :: (a :: sort 0) -> Ops a -> a -> a -> a;
+ecXor a pa = pa.this.xor;
+
+ecCompl :: (a :: sort 0) -> Ops a -> a -> a;
+ecCompl a pa = pa.this.not;
+
+ecZero :: (a :: sort 0) -> Ops a -> a;
+ecZero a pa = pa.this.zero;
 
 -- Sequences
-ecShiftL :: (m n :: Num) -> (a :: KType) -> seq m (ty a) -> seq n Bool -> seq m (ty a);
-ecShiftL (TCNum m) (TCNum n) a = bvShiftL m (ty a) n (ecZero a);
-ecShiftL TCInf (TCNum n) a = bvStreamShiftL (ty a) n;
+ecShiftL :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m a -> seq n Bool -> seq m a;
+ecShiftL (TCNum m) (TCNum n) a pa = bvShiftL m a n (ecZero a pa);
+ecShiftL TCInf (TCNum n) a _ = bvStreamShiftL a n;
 
-ecShiftR :: (m n :: Num) -> (a :: KType) -> seq m (ty a) -> seq n Bool -> seq m (ty a);
-ecShiftR (TCNum m) (TCNum n) a = bvShiftR m (ty a) n (ecZero a);
-ecShiftR TCInf (TCNum n) a = bvStreamShiftR (ty a) n (ecZero a);
+ecShiftR :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m a -> seq n Bool -> seq m a;
+ecShiftR (TCNum m) (TCNum n) a pa = bvShiftR m a n (ecZero a pa);
+ecShiftR TCInf (TCNum n) a pa = bvStreamShiftR a n (ecZero a pa);
 
-ecRotL :: (m n :: Num) -> (a :: KType) -> seq m (ty a) -> seq n Bool -> seq m (ty a);
-ecRotL (TCNum m) (TCNum n) a = bvRotateL m (ty a) n;
+ecRotL :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m a -> seq n Bool -> seq m a;
+ecRotL (TCNum m) (TCNum n) a _ = bvRotateL m a n;
 
-ecRotR :: (m n :: Num) -> (a :: KType) -> seq m (ty a) -> seq n Bool -> seq m (ty a);
-ecRotR (TCNum m) (TCNum n) a = bvRotateR m (ty a) n;
+ecRotR :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m a -> seq n Bool -> seq m a;
+ecRotR (TCNum m) (TCNum n) a _ = bvRotateR m a n;
 
-ecCat :: (m n :: Num) -> (a :: KType) -> seq m (ty a) -> seq n (ty a) -> seq (tcAdd m n) (ty a);
-ecCat (TCNum m) (TCNum n) a = append m n (ty a);
-ecCat (TCNum m) TCInf a = streamAppend (ty a) m;
+ecCat :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m a -> seq n a -> seq (tcAdd m n) a;
+ecCat (TCNum m) (TCNum n) a _ = append m n a;
+ecCat (TCNum m) TCInf a _ = streamAppend a m;
 
-ecSplitAt :: (m n :: Num) -> (a :: KType) -> seq (tcAdd m n) (ty a) -> #(seq m (ty a), seq n (ty a));
-ecSplitAt (TCNum m) (TCNum n) a xs = (take (ty a) m n xs, drop (ty a) m n xs);
-ecSplitAt (TCNum m) TCInf a xs = (streamTake (ty a) m xs, streamDrop (ty a) m xs);
+ecSplitAt :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq (tcAdd m n) a -> #(seq m a, seq n a);
+ecSplitAt (TCNum m) (TCNum n) a _ xs = (take a m n xs, drop a m n xs);
+ecSplitAt (TCNum m) TCInf a _ xs = (streamTake a m xs, streamDrop a m xs);
 
-ecJoin :: (m n :: Num) -> (a :: KType) -> seq m (seq n (ty a)) -> seq (tcMul m n) (ty a);
-ecJoin (TCNum m) (TCNum n) a = join m n (ty a);
-ecJoin TCInf (TCNum n) a =
+ecJoin :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m (seq n a) -> seq (tcMul m n) a;
+ecJoin (TCNum m) (TCNum n) a _ = join m n a;
+ecJoin TCInf (TCNum n) a _ =
   natCase
-    (\ (n'::Nat) -> Stream (Vec n' (ty a)) -> seq (ite Num (equalNat 0 n') (TCNum 0) TCInf) (ty a))
-      (\ (s::Stream (Vec 0 (ty a))) -> EmptyVec (ty a))
-      (\ (n'::Nat) -> \ (s::Stream (Vec (Succ n') (ty a))) -> streamJoin (ty a) n' s)
+    (\ (n'::Nat) -> Stream (Vec n' a) -> seq (ite Num (equalNat 0 n') (TCNum 0) TCInf) a)
+      (\ (s::Stream (Vec 0 a)) -> EmptyVec a)
+      (\ (n'::Nat) -> \ (s::Stream (Vec (Succ n') a)) -> streamJoin a n' s)
       n;
 
-ecSplit :: (m n :: Num) -> (a :: KType) -> seq (tcMul m n) (ty a) -> seq m (seq n (ty a));
-ecSplit (TCNum m) (TCNum n) a = split m n (ty a);
-ecSplit TCInf (TCNum n) a =
+ecSplit :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq (tcMul m n) a -> seq m (seq n a);
+ecSplit (TCNum m) (TCNum n) a _ = split m n a;
+ecSplit TCInf (TCNum n) a _ =
   natCase
-  (\(n :: Nat) -> seq (ite Num (equalNat 0 n) (TCNum 0) TCInf) (ty a) -> Stream (Vec n (ty a)))
-  (streamConst (Vec 0 (ty a))) (\(n :: Nat) -> streamSplit (ty a) (Succ n)) n;
+  (\(n :: Nat) -> seq (ite Num (equalNat 0 n) (TCNum 0) TCInf) a -> Stream (Vec n a))
+  (streamConst (Vec 0 a)) (\(n :: Nat) -> streamSplit a (Succ n)) n;
 
-ecReverse :: (n :: Num) -> (a :: KType) -> seq n (ty a) -> seq n (ty a);
-ecReverse (TCNum n) a = reverse n (ty a);
+ecReverse :: (n :: Num) -> (a :: sort 0) -> Ops a -> seq n a -> seq n a;
+ecReverse (TCNum n) a _ = reverse n a;
 
-ecTranspose :: (m n :: Num) -> (a :: KType) -> seq m (seq n (ty a)) -> seq n (seq m (ty a));
-ecTranspose (TCNum m) (TCNum n) a = transpose m n (ty a);
+ecTranspose :: (m n :: Num) -> (a :: sort 0) -> Ops a -> seq m (seq n a) -> seq n (seq m a);
+ecTranspose (TCNum m) (TCNum n) a _ = transpose m n a;
 -- TODO: other cases
 
-ecAt :: (n :: Num) -> (a :: KType) -> (i :: Num) -> seq n (ty a) -> seq i Bool -> ty a;
-ecAt (TCNum n) a (TCNum i) = bvAt n (ty a) i;
-ecAt TCInf a (TCNum i) = bvStreamGet (ty a) i;
+ecAt :: (n :: Num) -> (a :: sort 0) -> Ops a -> (i :: Num) -> seq n a -> seq i Bool -> a;
+ecAt (TCNum n) a _ (TCNum i) = bvAt n a i;
+ecAt TCInf a _ (TCNum i) = bvStreamGet a i;
 
-ecAtRange :: (n :: Num) -> (a :: KType) -> (m i :: Num) -> seq n (ty a) -> seq m (seq i Bool) -> seq m (ty a);
-ecAtRange n a m i xs = seqMap (seq i Bool) (ty a) m (ecAt n a i xs);
+ecAtRange :: (n :: Num) -> (a :: sort 0) -> Ops a -> (m i :: Num) -> seq n a -> seq m (seq i Bool) -> seq m a;
+ecAtRange n a pa m i xs = seqMap (seq i Bool) a m (ecAt n a pa i xs);
 
-ecAtBack :: (n :: Num) -> (a :: KType) -> (i :: Num) -> seq n (ty a) -> seq i Bool -> ty a;
-ecAtBack n a i xs = ecAt n a i (ecReverse n a xs);
+ecAtBack :: (n :: Num) -> (a :: sort 0) -> Ops a -> (i :: Num) -> seq n a -> seq i Bool -> a;
+ecAtBack n a pa i xs = ecAt n a pa i (ecReverse n a pa xs);
 
-ecAtRangeBack :: (n :: Num) -> (a :: KType) -> (m i :: Num) -> seq n (ty a) -> seq m (seq i Bool) -> seq m (ty a);
-ecAtRangeBack n a m i xs = seqMap (seq i Bool) (ty a) m (ecAtBack n a i xs);
+ecAtRangeBack :: (n :: Num) -> (a :: sort 0) -> Ops a -> (m i :: Num) -> seq n a -> seq m (seq i Bool) -> seq m a;
+ecAtRangeBack n a pa m i xs = seqMap (seq i Bool) a m (ecAtBack n a pa i xs);
 
 -- Static word sequences
 ecFromThen :: (first next bits len :: Num) -> seq len (seq bits Bool);
@@ -639,7 +636,7 @@ ecInfFromThen (TCNum n) first next =
     bvAdd n first (bvMul n (bvSub n next first) (bvNat n i)));
 
 -- Run-time error
-primitive ecError :: (a :: KType) -> (len :: Num) -> seq len (bitvector 8) -> ty a;
+primitive ecError :: (a :: sort 0) -> Ops a -> (len :: Num) -> seq len (bitvector 8) -> a;
 
 -- Polynomials
 ecPMul :: (a b :: Num) -> seq a Bool -> seq b Bool
@@ -653,25 +650,25 @@ ecPMod :: (a b :: Num) -> seq a Bool -> seq (tcAdd (TCNum 1) b) Bool -> seq b Bo
 ecPMod (TCNum a) (TCNum b) = bvPMod a b;
 
 -- Random values
-ecRandom :: (a :: KType) -> bitvector 32 -> ty a;
-ecRandom a _ = error (ty a) "Cryptol.random";
+ecRandom :: (a :: sort 0) -> Ops a -> bitvector 32 -> a;
+ecRandom a _ _ = error a "Cryptol.random";
 
 -- Trace function; simply return the final argument
-ecTrace :: (n :: Num) -> (a b :: KType) -> seq n (bitvector 8) -> ty a -> ty b -> ty b;
-ecTrace _ _ _ _ _ x = x;
+ecTrace :: (n :: Num) -> (a :: sort 0) -> Ops a -> (b :: sort 0) -> Ops b -> seq n (bitvector 8) -> a -> b -> b;
+ecTrace _ _ _ _ _ _ _ x = x;
 
 --------------------------------------------------------------------------------
 -- Extra primitives
 
 -- Array update
-ecUpdate :: (n :: Num) -> (a :: KType) -> (w :: Num)
-  -> seq n (ty a) -> seq w Bool -> ty a -> seq n (ty a);
-ecUpdate (TCNum n) a (TCNum w) = bvUpd n (ty a) w;
-ecUpdate TCInf     a (TCNum w) = bvStreamUpd (ty a) w;
-
-ecUpdateEnd :: (n :: Num) -> (a :: KType) -> (w :: Num)
-  -> seq n (ty a) -> seq w Bool -> ty a -> seq n (ty a);
-ecUpdateEnd (TCNum n) a (TCNum w) xs i y = upd n (ty a) xs (subNat (subNat n 1) (bvToNat w i)) y;
+ecUpdate :: (n :: Num) -> (a :: sort 0) -> Ops a -> (w :: Num)
+  -> seq n a -> seq w Bool -> a -> seq n a;
+ecUpdate (TCNum n) a _ (TCNum w) = bvUpd n a w;
+ecUpdate TCInf     a _ (TCNum w) = bvStreamUpd a w;
+
+ecUpdateEnd :: (n :: Num) -> (a :: sort 0) -> Ops a -> (w :: Num)
+  -> seq n a -> seq w Bool -> a -> seq n a;
+ecUpdateEnd (TCNum n) a _ (TCNum w) xs i y = upd n a xs (subNat (subNat n 1) (bvToNat w i)) y;
 
 -- Bitvector truncation
 ecTrunc :: (m n :: Num) -> seq (tcAdd m n) Bool -> seq n Bool;
diff --git a/src/Verifier/SAW/Cryptol.hs b/src/Verifier/SAW/Cryptol.hs
index 5336c74..8bd6d43 100644
--- a/src/Verifier/SAW/Cryptol.hs
+++ b/src/Verifier/SAW/Cryptol.hs
@@ -58,8 +58,8 @@ impossible name = fail ("impossible: " ++ name)
 -- | SharedTerms are paired with a deferred shift amount for loose variables
 data Env = Env
   { envT :: Map Int    (Term, Int) -- ^ Type variables are referenced by unique id
+  , envD :: Map Int    (Term, Int) -- ^ Dictionaries are referenced by unique id
   , envE :: Map C.Name (Term, Int) -- ^ Term variables are referenced by name
-  , envP :: Map C.Prop (Term, Int) -- ^ Bound propositions are referenced implicitly by their types
   , envC :: Map C.Name C.Schema    -- ^ Cryptol type environment
   }
 
@@ -73,13 +73,21 @@ liftTerm (t, j) = (t, j + 1)
 liftEnv :: Env -> Env
 liftEnv env =
   Env { envT = fmap liftTerm (envT env)
+      , envD = fmap liftTerm (envD env)
       , envE = fmap liftTerm (envE env)
-      , envP = fmap liftTerm (envP env)
       , envC = envC env
       }
 
-bindTParam :: SharedContext -> C.TParam -> Env -> IO Env
-bindTParam sc tp env = do
+bindKTypeParam :: SharedContext -> C.TParam -> Env -> IO Env
+bindKTypeParam sc tp env = do
+  let env' = liftEnv (liftEnv env)
+  v <- scLocalVar sc 1
+  d <- scLocalVar sc 0
+  return $ env' { envT = Map.insert (C.tpUnique tp) (v, 0) (envT env')
+                , envD = Map.insert (C.tpUnique tp) (d, 0) (envD env') }
+
+bindKNumParam :: SharedContext -> C.TParam -> Env -> IO Env
+bindKNumParam sc tp env = do
   let env' = liftEnv env
   v <- scLocalVar sc 0
   return $ env' { envT = Map.insert (C.tpUnique tp) (v, 0) (envT env') }
@@ -90,22 +98,8 @@ bindName sc name schema env = do
   v <- scLocalVar sc 0
   return $ env' { envE = Map.insert name (v, 0) (envE env'), envC = Map.insert name schema (envC env') }
 
-bindProp :: SharedContext -> C.Prop -> Env -> IO Env
-bindProp sc prop env = do
-  let env' = liftEnv env
-  v <- scLocalVar sc 0
-  return $ env' { envP = Map.insert prop (v, 0) (envP env') }
-
 --------------------------------------------------------------------------------
 
-importKind :: SharedContext -> C.Kind -> IO Term
-importKind sc kind =
-  case kind of
-    C.KType       -> scDataTypeApp sc "Cryptol.KType" []
-    C.KNum        -> scDataTypeApp sc "Cryptol.Num" []
-    C.KProp       -> scSort sc (mkSort 0)
-    (C.:->) k1 k2 -> join $ scFun sc <$> importKind sc k1 <*> importKind sc k2
-
 importTFun :: SharedContext -> C.TFun -> IO Term
 importTFun sc tf =
   case tf of
@@ -121,6 +115,7 @@ importTFun sc tf =
     C.TCLenFromThen   -> scGlobalDef sc "Cryptol.tcLenFromThen"
     C.TCLenFromThenTo -> scGlobalDef sc "Cryptol.tcLenFromThenTo"
 
+-- | Translate size types to SAW values of type Num, value types to SAW types of sort 0.
 importType :: SharedContext -> Env -> C.Type -> IO Term
 importType sc env ty =
   case ty of
@@ -131,29 +126,23 @@ importType sc env ty =
                               Just (t, j) -> incVars sc 0 j t
                               Nothing -> fail "internal error: importType TVBound"
     C.TUser _ _ t  -> go t
-    C.TRec fs      -> importTRec sc env (Map.assocs (Map.fromList fs))
+    C.TRec fs -> scRecordType sc =<< traverse go tm
+      where tm = Map.fromList [ (C.unpackIdent n, t) | (n, t) <- fs ]
     C.TCon tcon tyargs ->
       case tcon of
         C.TC tc ->
           case tc of
             C.TCNum n    -> scCtorApp sc "Cryptol.TCNum" =<< sequence [scNat sc (fromInteger n)]
             C.TCInf      -> scCtorApp sc "Cryptol.TCInf" []
-            C.TCBit      -> scCtorApp sc "Cryptol.TCBit" []
-            C.TCSeq      -> scCtorApp sc "Cryptol.TCSeq" =<< traverse go tyargs
-            C.TCFun      -> scCtorApp sc "Cryptol.TCFun" =<< traverse go tyargs
-            C.TCTuple _n -> importTCTuple sc env tyargs
+            C.TCBit      -> scBoolType sc
+            C.TCSeq      -> scGlobalApply sc "Cryptol.seq" =<< traverse go tyargs
+            C.TCFun      -> do a <- go (tyargs !! 0)
+                               b <- go (tyargs !! 1)
+                               scFun sc a b
+            C.TCTuple _n -> scTuple sc =<< traverse go tyargs
             C.TCNewtype (C.UserTC _qn _k) -> unimplemented "TCNewtype" -- user-defined, @T@
-        C.PC pc ->
-          case pc of
-            C.PEqual         -> impossible "importType PEqual"
-            C.PNeq           -> impossible "importType PNeq"
-            C.PGeq           -> impossible "importType PGeq"
-            C.PFin           -> impossible "importType PFin"
-            C.PHas _selector -> unimplemented "PHas"
-            C.PArith         -> scDataTypeApp sc "Cryptol.PArith" =<< traverse go tyargs -- @Arith _@
-            C.PCmp           -> scDataTypeApp sc "Cryptol.PCmp"   =<< traverse go tyargs -- @Cmp _@
-            C.PAnd           -> impossible "importType PAnd"
-            C.PTrue          -> impossible "importType PTrue"
+        C.PC _pc ->
+          impossible "importType Prop"
         C.TF tf ->
           do tf' <- importTFun sc tf
              tyargs' <- traverse go tyargs
@@ -163,21 +152,61 @@ importType sc env ty =
   where
     go = importType sc env
 
--- | Precondition: list argument should be sorted by field name
-importTRec :: SharedContext -> Env -> [(C.Ident, C.Type)] -> IO Term
-importTRec sc _env [] = scCtorApp sc "Cryptol.TCEmpty" []
-importTRec sc env ((n, t) : fs) = do
-  n' <- scString sc (C.unpackIdent n)
-  t' <- importType sc env t
-  fs' <- importTRec sc env fs
-  scCtorApp sc "Cryptol.TCField" [n', t', fs']
-
-importTCTuple :: SharedContext -> Env -> [C.Type] -> IO Term
-importTCTuple sc _env [] = scCtorApp sc "Cryptol.TCUnit" []
-importTCTuple sc env (t : ts) = do
-  t' <- importType sc env t
-  ts' <- importTCTuple sc env ts
-  scCtorApp sc "Cryptol.TCPair" [t', ts']
+-- | Translate value types to SAW dictionaries of type Ops a.
+importOps :: SharedContext -> Env -> C.Type -> IO Term
+importOps sc env ty =
+  case ty of
+    C.TVar tvar ->
+      case tvar of
+        C.TVFree{} {- Int Kind (Set TVar) Doc -} -> unimplemented "importOps TVFree"
+        C.TVBound i _k   -> case Map.lookup i (envD env) of
+                              Just (t, j) -> incVars sc 0 j t
+                              Nothing -> fail "internal error: importOps TVBound"
+    C.TUser _ _ t  -> importOps sc env t
+    C.TRec fs -> importTRec [ (C.unpackIdent n, t) | (n, t) <- fs ]
+    C.TCon tcon tyargs ->
+      case tcon of
+        C.TC tc ->
+          case tc of
+            C.TCNum _n   -> impossible "importOps TCNum"
+            C.TCInf      -> impossible "importOps TCInf"
+            C.TCBit      -> scGlobalApply sc "Cryptol.OpsBit" []
+            C.TCSeq      -> do n <- importType sc env (tyargs !! 0)
+                               a <- importType sc env (tyargs !! 1)
+                               pa <- importOps sc env (tyargs !! 1)
+                               scGlobalApply sc "Cryptol.OpsSeq" [n, a, pa]
+            C.TCFun      -> do a <- importType sc env (tyargs !! 0)
+                               b <- importType sc env (tyargs !! 1)
+                               pb <- importOps sc env (tyargs !! 1)
+                               scGlobalApply sc "Cryptol.OpsFun" [a, b, pb]
+            C.TCTuple _n -> importTCTuple tyargs
+            C.TCNewtype (C.UserTC _qn _k) -> unimplemented "TCNewtype" -- user-defined, @T@
+        C.PC _pc ->
+          impossible "importOps Prop"
+        C.TF _tf ->
+          impossible "importOps TF"
+        C.TError _k _msg ->
+          impossible "importOps TError"
+  where
+    -- | Precondition: list argument should be sorted by field name
+    importTRec :: [(String, C.Type)] -> IO Term
+    importTRec [] = scCtorApp sc "Cryptol.TCEmpty" []
+    importTRec ((n, t) : fs) = do
+      s <- scString sc n
+      a <- importType sc env t
+      pa <- importOps sc env t
+      b <- scRecordType sc =<< traverse (importType sc env) (Map.fromList fs)
+      pb <- importTRec fs
+      scGlobalApply sc "Cryptol.OpsField" [s, a, b, pa, pb]
+
+    importTCTuple :: [C.Type] -> IO Term
+    importTCTuple [] = scGlobalApply sc "Cryptol.OpsUnit" []
+    importTCTuple (t : ts) = do
+      a <- importType sc env t
+      pa <- importOps sc env t
+      b <- scTuple sc =<< traverse (importType sc env) ts
+      pb <- importTCTuple ts
+      scGlobalApply sc "Cryptol.OpsPair" [a, b, pa, pb]
 
 nameToString :: C.Name -> String
 nameToString = C.unpackIdent . C.nameIdent
@@ -186,51 +215,26 @@ tparamToString :: C.TParam -> String
 --tparamToString tp = maybe "_" nameToString (C.tpName tp)
 tparamToString tp = maybe ("u" ++ show (C.tpUnique tp)) nameToString (C.tpName tp)
 
-importType' :: SharedContext -> Env -> C.Type -> IO Term
-importType' sc env t = do
-  t' <- importType sc env t
-  scGlobalApply sc "Cryptol.ty" [t']
-
-isErasedProp :: C.Prop -> Bool
-isErasedProp prop =
-  case prop of
-    (C.pIsArith -> Just _) -> False
-    (C.pIsCmp   -> Just _) -> False
-    _ -> True
-
-importPropsType :: SharedContext -> Env -> [C.Prop] -> C.Type -> IO Term
-importPropsType sc env [] ty = importType' sc env ty
-importPropsType sc env (prop : props) ty
-  | isErasedProp prop = importPropsType sc env props ty
-  | otherwise = do
-    p <- importType sc env prop
-    t <- importPropsType sc env props ty
-    scFun sc p t
-
-importPolyType :: SharedContext -> Env -> [C.TParam] -> [C.Prop] -> C.Type -> IO Term
-importPolyType sc env [] props ty = importPropsType sc env props ty
-importPolyType sc env (tp : tps) props ty = do
-  k <- importKind sc (C.tpKind tp)
-  env' <- bindTParam sc tp env
-  t <- importPolyType sc env' tps props ty
-  scPi sc (tparamToString tp) k t
+importPolyType :: SharedContext -> Env -> [C.TParam] -> C.Type -> IO Term
+importPolyType sc env [] ty = importType sc env ty
+importPolyType sc env (tp : tps) ty =
+  case C.tpKind tp of
+    C.KType       -> do env' <- bindKTypeParam sc tp env
+                        k1 <- scSort sc (mkSort 0)
+                        v0 <- scLocalVar sc 0
+                        k2 <- scGlobalApply sc "Cryptol.Ops" [v0]
+                        ty' <- importPolyType sc env' tps ty
+                        let s = tparamToString tp
+                        scPi sc s k1 =<< scPi sc ("_" ++ s) k2 ty'
+    C.KNum        -> do env' <- bindKNumParam sc tp env
+                        k <- scDataTypeApp sc "Cryptol.Num" []
+                        ty' <- importPolyType sc env' tps ty
+                        scPi sc (tparamToString tp) k ty'
+    C.KProp       -> impossible "importPolyType: KProp"
+    (C.:->) _ _   -> impossible "importPolyType: arrow kind"
 
 importSchema :: SharedContext -> Env -> C.Schema -> IO Term
-importSchema sc env (C.Forall tparams props ty) = importPolyType sc env tparams props ty
-
-proveProp :: SharedContext -> Env -> C.Prop -> IO Term
-proveProp sc env prop =
-  case Map.lookup prop (envP env) of
-    Just (prf, j) -> incVars sc 0 j prf
-    Nothing ->
-      case prop of
-        (C.pIsArith -> Just t)
-          -> scGlobalApply sc "Cryptol.ePArith" =<< sequence [ty t]
-        (C.pIsCmp -> Just t)
-          -> scGlobalApply sc "Cryptol.ePCmp" =<< sequence [ty t]
-        _ -> fail "proveProp: unknown proposition"
-  where
-    ty = importType sc env
+importSchema sc env (C.Forall tparams _props ty) = importPolyType sc env tparams ty
 
 importPrimitive :: SharedContext -> C.Name -> IO Term
 importPrimitive sc (C.asPrim -> Just nm) =
@@ -304,7 +308,7 @@ importPrimitive _ nm =
 importExpr :: SharedContext -> Env -> C.Expr -> IO Term
 importExpr sc env expr =
   case expr of
-    C.EList es t                -> do t' <- importType' sc env t
+    C.EList es t                -> do t' <- importType sc env t
                                       es' <- traverse go es
                                       scVector sc t' es'
     C.ETuple es                 -> scTuple sc =<< traverse go es
@@ -332,12 +336,12 @@ importExpr sc env expr =
                                       (n, a) <- case C.tIsSeq t of
                                                   Just (n, a) -> return (n, a)
                                                   Nothing -> fail "ListSel: not a list type"
-                                      a' <- importType' sc env a
+                                      a' <- importType sc env a
                                       n' <- importType sc env n
                                       e' <- importExpr sc env e
                                       i' <- scNat sc (fromIntegral i)
                                       scGlobalApply sc "Cryptol.eListSel" [a', n', e', i']
-    C.EIf e1 e2 e3              -> do t' <- importType' sc env (fastTypeOf (envC env) e2)
+    C.EIf e1 e2 e3              -> do t' <- importType sc env (fastTypeOf (envC env) e2)
                                       e1' <- importExpr sc env e1
                                       e2' <- importExpr sc env e2
                                       e3' <- importExpr sc env e3
@@ -347,34 +351,46 @@ importExpr sc env expr =
       case Map.lookup qname (envE env) of
         Just (e', j)                -> incVars sc 0 j e'
         Nothing                     -> fail $ "internal error: unknown variable: " ++ show qname
-    C.ETAbs tp e                    -> do k <- importKind sc (C.tpKind tp)
-                                          env' <- bindTParam sc tp env
-                                          e' <- importExpr sc env' e
-                                          scLambda sc (tparamToString tp) k e'
-    C.ETApp e t                     -> join $ scApply sc <$> go e <*> ty t
+    C.ETAbs tp e                    -> case C.tpKind tp of
+                                         C.KType -> do
+                                           env' <- bindKTypeParam sc tp env
+                                           k1 <- scSort sc (mkSort 0)
+                                           v0 <- scLocalVar sc 0
+                                           k2 <- scGlobalApply sc "Cryptol.Ops" [v0]
+                                           e' <- importExpr sc env' e
+                                           let s = tparamToString tp
+                                           scLambda sc s k1 =<< scLambda sc ("_" ++ s) k2 e'
+                                         C.KNum -> do
+                                           env' <- bindKNumParam sc tp env
+                                           k <- scDataTypeApp sc "Cryptol.Num" []
+                                           e' <- importExpr sc env' e
+                                           scLambda sc (tparamToString tp) k e'
+                                         _ -> impossible "importExpr ETAbs: invalid kind"
+    C.ETApp e t                     -> case fastSchemaOf (envC env) e of
+                                         C.Forall (tp1 : _) _ _ ->
+                                           case C.tpKind tp1 of
+                                             C.KType -> do
+                                               e' <- importExpr sc env e
+                                               t' <- importType sc env t
+                                               d' <- importOps sc env t
+                                               scApplyAll sc e' [t', d']
+                                             C.KNum -> do
+                                               e' <- importExpr sc env e
+                                               t' <- importType sc env t
+                                               scApply sc e' t'
+                                             _ -> impossible "importExpr ETApp: invalid kind"
+                                         _ -> impossible "importExpr ETApp: monomorphic type"
     C.EApp e1 e2                    -> join $ scApply sc <$> go e1 <*> go e2
-    C.EAbs x t e                    -> do t' <- importType' sc env t
+    C.EAbs x t e                    -> do t' <- importType sc env t
                                           env' <- bindName sc x (C.Forall [] [] t) env
                                           e' <- importExpr sc env' e
                                           scLambda sc (nameToString x) t' e'
-    C.EProofAbs prop e1
-      | isErasedProp prop           -> do importExpr sc env e1
-      | otherwise                   -> do p <- importType sc env prop
-                                          env' <- bindProp sc prop env
-                                          e <- importExpr sc env' e1
-                                          scLambda sc "_P" p e
-    C.EProofApp e1                  -> case fastSchemaOf (envC env) e1 of
-                                         C.Forall [] (p1 : _) _
-                                           | isErasedProp p1 -> importExpr sc env e1
-                                           | otherwise ->
-                                             do e <- importExpr sc env e1
-                                                prf <- proveProp sc env p1
-                                                scApply sc e prf
-                                         s -> fail $ "EProofApp: invalid type: " ++ show (e1, s)
+    C.EProofAbs _prop e1            -> importExpr sc env e1
+    C.EProofApp e1                  -> importExpr sc env e1
 {-
     C.ECast e1 t2                   -> do let t1 = fastTypeOf (envC env) e1
-                                          t1' <- importType' sc env t1
-                                          t2' <- importType' sc env t2
+                                          t1' <- importType sc env t1
+                                          t2' <- importType sc env t2
                                           e1' <- go e1
                                           aeq <- pure alphaEquiv <*> scWhnf sc t1' <*> scWhnf sc t2'
                                           if aeq
@@ -385,7 +401,6 @@ importExpr sc env expr =
                                           importExpr sc env' e
   where
     go = importExpr sc env
-    ty = importType sc env
 
 mapTupleSelector :: SharedContext -> Env -> Int -> C.Type -> IO Term
 mapTupleSelector sc env i = fmap fst . go
@@ -395,22 +410,22 @@ mapTupleSelector sc env i = fmap fst . go
       case C.tNoUser t of
         (C.tIsSeq -> Just (n, a)) -> do
           (f, b) <- go a
-          a' <- importType' sc env a
-          b' <- importType' sc env b
+          a' <- importType sc env a
+          b' <- importType sc env b
           n' <- importType sc env n
           g <- scGlobalApply sc "Cryptol.seqMap" [a', b', n', f]
           return (g, C.tSeq n b)
         (C.tIsFun -> Just (n, a)) -> do
           (f, b) <- go a
-          a' <- importType' sc env a
-          b' <- importType' sc env b
-          n' <- importType' sc env n
+          a' <- importType sc env a
+          b' <- importType sc env b
+          n' <- importType sc env n
           g <- scGlobalApply sc "Cryptol.compose" [n', a', b', f]
           return (g, C.tFun n b)
         (C.tIsTuple -> Just ts) -> do
           x <- scLocalVar sc 0
           y <- scTupleSelector sc x (i+1)
-          t' <- importType' sc env t
+          t' <- importType sc env t
           f <- scLambda sc "x" t' y
           return (f, ts !! i)
         _ -> fail $ unwords ["importExpr: invalid tuple selector", show i, show t]
@@ -423,22 +438,22 @@ mapRecordSelector sc env i = fmap fst . go
       case C.tNoUser t of
         (C.tIsSeq -> Just (n, a)) -> do
           (f, b) <- go a
-          a' <- importType' sc env a
-          b' <- importType' sc env b
+          a' <- importType sc env a
+          b' <- importType sc env b
           n' <- importType sc env n
           g <- scGlobalApply sc "Cryptol.seqMap" [a', b', n', f]
           return (g, C.tSeq n b)
         (C.tIsFun -> Just (n, a)) -> do
           (f, b) <- go a
-          a' <- importType' sc env a
-          b' <- importType' sc env b
-          n' <- importType' sc env n
+          a' <- importType sc env a
+          b' <- importType sc env b
+          n' <- importType sc env n
           g <- scGlobalApply sc "Cryptol.compose" [n', a', b', f]
           return (g, C.tFun n b)
         C.TRec ts | Just b <- lookup i ts -> do
           x <- scLocalVar sc 0
           y <- scRecordSelect sc x (C.unpackIdent i)
-          t' <- importType' sc env t
+          t' <- importType sc env t
           f <- scLambda sc "x" t' y
           return (f, b)
         _ -> fail $ unwords ["importExpr: invalid record selector", show i, show t]
@@ -559,12 +574,12 @@ importComp sc env lenT elemT expr mss =
          zipAll [branch] =
            do (xs, len, ty, args) <- importMatches sc env branch
               m <- importType sc env len
-              a <- importType' sc env ty
+              a <- importType sc env ty
               return (xs, m, a, [args])
          zipAll (branch : branches) =
            do (xs, len, ty, args) <- importMatches sc env branch
               m <- importType sc env len
-              a <- importType' sc env ty
+              a <- importType sc env ty
               (ys, n, b, argss) <- zipAll branches
               zs <- scGlobalApply sc "Cryptol.seqZip" [a, b, m, n, xs, ys]
               mn <- scGlobalApply sc "Cryptol.tcMin" [m, n]
@@ -572,11 +587,11 @@ importComp sc env lenT elemT expr mss =
               return (zs, mn, ab, args : argss)
      (xs, n, a, argss) <- zipAll mss
      f <- lambdaTuples sc env elemT expr argss
-     b <- importType' sc env elemT
+     b <- importType sc env elemT
      ys <- scGlobalApply sc "Cryptol.seqMap" [a, b, n, f, xs]
      -- The resulting type might not match the annotation, so we coerce
      t1 <- scGlobalApply sc "Cryptol.seq" [n, b]
-     t2 <- importType' sc env (C.tSeq lenT elemT)
+     t2 <- importType sc env (C.tSeq lenT elemT)
      scGlobalApply sc "Prelude.unsafeCoerce" [t1, t2, ys]
 
 lambdaTuples :: SharedContext -> Env -> C.Type -> C.Expr -> [[(C.Name, C.Type)]] -> IO Term
@@ -585,23 +600,23 @@ lambdaTuples sc env ty expr (args : argss) =
   do f <- lambdaTuple sc env ty expr argss args
      if null args || null argss
        then return f
-       else do a <- importType' sc env (tNestedTuple (map snd args))
-               b <- importType' sc env (tNestedTuple (map (tNestedTuple . map snd) argss))
-               c <- importType' sc env ty
+       else do a <- importType sc env (tNestedTuple (map snd args))
+               b <- importType sc env (tNestedTuple (map (tNestedTuple . map snd) argss))
+               c <- importType sc env ty
                scGlobalApply sc "Prelude.uncurry" [a, b, c, f]
 
 lambdaTuple :: SharedContext -> Env -> C.Type -> C.Expr -> [[(C.Name, C.Type)]] -> [(C.Name, C.Type)] -> IO Term
 lambdaTuple sc env ty expr argss [] = lambdaTuples sc env ty expr argss
 lambdaTuple sc env ty expr argss ((x, t) : args) =
-  do a <- importType' sc env t
+  do a <- importType sc env t
      env' <- bindName sc x (C.Forall [] [] t) env
      e <- lambdaTuple sc env' ty expr argss args
      f <- scLambda sc (nameToString x) a e
      if null args
         then return f
-        else do b <- importType' sc env (tNestedTuple (map snd args))
+        else do b <- importType sc env (tNestedTuple (map snd args))
                 let tuple = tNestedTuple (map (tNestedTuple . map snd) argss)
-                c <- importType' sc env (if null argss then ty else C.tFun tuple ty)
+                c <- importType sc env (if null argss then ty else C.tFun tuple ty)
                 scGlobalApply sc "Prelude.uncurry" [a, b, c, f]
 
 tNestedTuple :: [C.Type] -> C.Type
@@ -628,12 +643,12 @@ importMatches sc env (C.From name _len _eltty expr : matches) = do
                    Just x -> return x
                    Nothing -> fail $ "internal error: From: " ++ show (fastTypeOf (envC env) expr)
   m <- importType sc env len1
-  a <- importType' sc env ty1
+  a <- importType sc env ty1
   xs <- importExpr sc env expr
   env' <- bindName sc name (C.Forall [] [] ty1) env
   (body, len2, ty2, args) <- importMatches sc env' matches
   n <- importType sc env len2
-  b <- importType' sc env ty2
+  b <- importType sc env ty2
   f <- scLambda sc (nameToString name) a body
   result <- scGlobalApply sc "Cryptol.from" [a, b, m, n, xs, f]
   return (result, C.tMul len1 len2, C.tTuple [ty1, ty2], (name, ty1) : args)
@@ -646,7 +661,7 @@ importMatches sc env [C.Let decl]
      ty1 <- case C.dSignature decl of
               C.Forall [] [] ty1 -> return ty1
               _ -> unimplemented "polymorphic Let"
-     a <- importType' sc env ty1
+     a <- importType sc env ty1
      result <- scGlobalApply sc "Prelude.single" [a, e]
      return (result, C.tOne, ty1, [(C.dName decl, ty1)])
 
@@ -659,11 +674,11 @@ importMatches sc env (C.Let decl : matches) =
      ty1 <- case C.dSignature decl of
               C.Forall [] [] ty1 -> return ty1
               _ -> unimplemented "polymorphic Let"
-     a <- importType' sc env ty1
+     a <- importType sc env ty1
      env' <- bindName sc (C.dName decl) (C.dSignature decl) env
      (body, len, ty2, args) <- importMatches sc env' matches
      n <- importType sc env len
-     b <- importType' sc env ty2
+     b <- importType sc env ty2
      f <- scLambda sc (nameToString (C.dName decl)) a body
      result <- scGlobalApply sc "Cryptol.mlet" [a, b, n, e, f]
      return (result, len, C.tTuple [ty1, ty2], (C.dName decl, ty1) : args)