diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
index 1e2e56c61e..77cc116adb 100644
--- a/cryptol-saw-core/saw/Cryptol.sawcore
+++ b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -14,10 +14,10 @@ const a b x y = x;
 compose : (a b c : sort 0) -> (b -> c) -> (a -> b) -> (a -> c);
 compose _ _ _ f g x = f (g x);
 
-bvExp : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
-bvExp n x y = foldr Bool (Vec n Bool) n
-  (\ (b : Bool) -> \ (a : Vec n Bool) ->
-    ite (Vec n Bool) b (bvMul n x (bvMul n a a)) (bvMul n a a))
+bvExp : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
+bvExp n x y = foldr Bool (Vec Bool n) n
+  (\ (b : Bool) -> \ (a : Vec Bool n) ->
+    ite (Vec Bool n) b (bvMul n x (bvMul n a a)) (bvMul n a a))
   (bvNat n 1)
   (reverse n Bool y);
 
@@ -239,11 +239,11 @@ tcLt = binaryNumPred ltNat (\ (x:Nat) -> True) (\ (y:Nat) -> False) True;
 
 seq : Num -> sort 0 -> sort 0;
 seq num a =
-  Num#rec1 (\ (num:Num) -> sort 0) (\ (n:Nat) -> Vec n a) (Stream a) num;
+  Num#rec1 (\ (num:Num) -> sort 0) (\ (n:Nat) -> Vec a n) (Stream a) num;
 
 -- FIXME: this rule should be derived by scDefRewriteRules
-seq_TCNum : (n:Nat) -> (a:sort 0) -> Eq (sort 0) (seq (TCNum n) a) (Vec n a);
-seq_TCNum n a = Refl (sort 0) (Vec n a);
+seq_TCNum : (n:Nat) -> (a:sort 0) -> Eq (sort 0) (seq (TCNum n) a) (Vec a n);
+seq_TCNum n a = Refl (sort 0) (Vec a n);
 seq_TCInf : (a:sort 0) -> Eq (sort 0) (seq TCInf a) (Stream a);
 seq_TCInf a = Refl (sort 0) (Stream a);
 
@@ -364,25 +364,25 @@ from a b m n =
     (\ (m:Num) -> seq m a -> (a -> seq n b) -> seq (tcMul m n) #(a, b))
     (\ (m:Nat) ->
        Num#rec
-         (\ (n:Num) -> Vec m a -> (a -> seq n b) ->
+         (\ (n:Num) -> Vec a m -> (a -> seq n b) ->
                         seq (tcMul (TCNum m) n) #(a, b))
          -- Case 1: (TCNum m, TCNum n)
          (\ (n:Nat) ->
-            \ (xs : Vec m a) ->
-            \ (k : a -> Vec n b) ->
+            \ (xs : Vec a m) ->
+            \ (k : a -> Vec b n) ->
               join m n #(a, b)
-                   (map a (Vec n #(a, b))
+                   (map a (Vec #(a, b) n)
                         (\ (x : a) ->
                            map b #(a, b) (\ (y : b) -> (x, y)) n (k x))
                         m xs))
          -- Case 2: n = (TCNum m, TCInf)
          (natCase
-            (\ (m':Nat) -> (Vec m' a -> (a -> Stream b) ->
+            (\ (m':Nat) -> (Vec a m' -> (a -> Stream b) ->
                seq (if0Nat Num m' (TCNum 0) TCInf) #(a, b)))
-            (\ (xs : Vec 0 a) ->
+            (\ (xs : Vec a 0) ->
              \ (k : a -> Stream b) -> EmptyVec #(a, b))
             (\ (m' : Nat) ->
-             \ (xs : Vec (Succ m') a) ->
+             \ (xs : Vec a (Succ m')) ->
              \ (k : a -> Stream b) ->
                (\ (x : a) -> streamMap b #(a, b) (\ (y:b) -> (x, y)) (k x))
                (at (Succ m') a xs 0))
@@ -393,17 +393,17 @@ from a b m n =
        -- Case 3: (TCInf, TCNum n)
        (\ (n:Nat) ->
           natCase
-            (\ (n':Nat) -> (Stream a -> (a -> Vec n' b) ->
+            (\ (n':Nat) -> (Stream a -> (a -> Vec b n') ->
                 seq (if0Nat Num n' (TCNum 0) TCInf) #(a, b)))
             (\ (xs : Stream a) ->
-             \ (k : a -> Vec 0 b) -> EmptyVec #(a, b))
+             \ (k : a -> Vec b 0) -> EmptyVec #(a, b))
             (\ (n' : Nat) ->
              \ (xs : Stream a) ->
-             \ (k : a -> Vec (Succ n') b) ->
+             \ (k : a -> Vec b (Succ n')) ->
                streamJoin
                  #(a, b) n'
                  (streamMap
-                    a (Vec (Succ n') #(a, b))
+                    a (Vec #(a, b) (Succ n'))
                     (\ (x:a) ->
                        map b #(a, b) (\ (y:b) -> (x, y)) (Succ n') (k x))
                     xs))
@@ -421,7 +421,7 @@ mlet : (a b : isort 0) -> (n : Num) -> a -> (a -> seq n b) -> seq n #(a, b);
 mlet a b n =
   Num#rec
     (\ (n:Num) -> a -> (a -> seq n b) -> seq n #(a, b))
-    (\ (n:Nat) -> \ (x:a) -> \ (f:a -> Vec n b) ->
+    (\ (n:Nat) -> \ (x:a) -> \ (f:a -> Vec b n) ->
        map b #(a, b) (\ (y : b) -> (x, y)) n (f x))
     (\ (x:a) -> \ (f:a -> Stream b) ->
        streamMap b #(a, b) (\ (y : b) -> (x, y)) (f x))
@@ -434,21 +434,21 @@ seqZip a b m n =
     (\ (m:Num) -> seq m a -> seq n b -> seq (tcMin m n) #(a, b))
     (\ (m : Nat) ->
        Num#rec
-         (\ (n:Num) -> Vec m a -> seq n b -> seq (tcMin (TCNum m) n) #(a, b))
+         (\ (n:Num) -> Vec a m -> seq n b -> seq (tcMin (TCNum m) n) #(a, b))
          (\ (n:Nat) -> zip a b m n)
-         (\ (xs:Vec m a) -> \ (ys:Stream b) ->
+         (\ (xs:Vec a m) -> \ (ys:Stream b) ->
             gen m #(a, b) (\ (i : Nat) -> (at m a xs i, streamGet b ys i)))
          n)
     (Num#rec
        (\ (n:Num) -> Stream a -> seq n b -> seq (tcMin TCInf n) #(a, b))
        (\ (n:Nat) ->
-        \ (xs:Stream a) -> \ (ys:Vec n b) ->
+        \ (xs:Stream a) -> \ (ys:Vec b n) ->
           gen n #(a, b) (\ (i : Nat) -> (streamGet a xs i, at n b ys i)))
        (streamMap2 a b #(a, b) (\ (x:a) -> \ (y:b) -> (x, y)))
        n)
     m;
 
-zipSame : (a b : isort 0) -> (n : Nat) -> Vec n a -> Vec n b -> Vec n #(a, b);
+zipSame : (a b : isort 0) -> (n : Nat) -> Vec a n -> Vec b n -> Vec #(a, b) n;
 zipSame a b n x y = gen n #(a, b) (\ (i : Nat) -> (at n a x i, at n b y i));
 
 seqZipSame : (a b : isort 0) -> (n : Num) -> seq n a -> seq n b -> seq n #(a, b);
@@ -533,14 +533,14 @@ integerCmp x y k = or (intLt x y) (and (intEq x y) k);
 rationalCmp : Rational -> Rational -> Bool -> Bool;
 rationalCmp x y k = or (rationalLt x y) (and (rationalEq x y) k);
 
-bvCmp : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool -> Bool;
+bvCmp : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool -> Bool;
 bvCmp n x y k = or (bvult n x y) (and (bvEq n x y) k);
 
-bvSCmp : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool -> Bool;
+bvSCmp : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool -> Bool;
 bvSCmp n x y k = or (bvslt n x y) (and (bvEq n x y) k);
 
 vecCmp : (n : Nat) -> (a : isort 0) -> (a -> a -> Bool -> Bool)
-       -> (Vec n a -> Vec n a -> Bool -> Bool);
+       -> (Vec a n -> Vec a n -> 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);
@@ -549,7 +549,7 @@ vecLt :
   (n : Nat) -> (a : isort 0) ->
   (a -> a -> Bool -> Bool) ->
   (a -> a -> Bool) ->
-  (Vec n a -> Vec n a -> Bool);
+  (Vec a n -> Vec a n -> Bool);
 vecLt n a f g xs ys =
   foldr (Bool -> Bool) Bool n (\ (f : Bool -> Bool) -> f) False
     (zipWith a a (Bool -> Bool) f n xs ys);
@@ -636,7 +636,8 @@ PEqIntModNum : (num : Num) -> PEq (IntModNum num);
 PEqIntModNum num =
   Num#rec1 (\ (n : Num) -> PEq (IntModNum n)) PEqIntMod PEqInteger num;
 
-PEqVec : (n : Nat) -> (a : isort 0) -> PEq a -> PEq (Vec n a);
+
+PEqVec : (n : Nat) -> (a : isort 0) -> PEq a -> PEq (Vec a n);
 PEqVec n a pa = { eq = vecEq n a pa.eq };
 
 PEqSeq : (n : Num) -> (a : isort 0) -> PEq a -> PEq (seq n a);
@@ -646,7 +647,7 @@ PEqSeq n =
            (\ (a:isort 0) (pa : PEq a) -> error (PEq (Stream a)) "invalid Eq instance")
            n;
 
-PEqWord : (n : Nat) -> PEq (Vec n Bool);
+PEqWord : (n : Nat) -> PEq (Vec Bool n);
 PEqWord n = { eq = bvEq n };
 
 PEqSeqBool : (n : Num) -> PEq (seq n Bool);
@@ -710,12 +711,12 @@ PCmpInteger = { cmpEq = PEqInteger, cmp = integerCmp, le = intLe, lt = intLt };
 PCmpRational : PCmp Rational;
 PCmpRational = { cmpEq = PEqRational, cmp = rationalCmp, le = rationalLe, lt = rationalLt };
 
-PCmpVec : (n : Nat) -> (a : isort 0) -> PCmp a -> PCmp (Vec n a);
+PCmpVec : (n : Nat) -> (a : isort 0) -> PCmp a -> PCmp (Vec a n);
 PCmpVec n a pa =
   { cmpEq = PEqVec n a pa.cmpEq
   , cmp = vecCmp n a pa.cmp
-  , le = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.cmp x y True
-  , lt = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.cmp x y False
+  , le = \ (x : Vec a n) -> \ (y : Vec a n) -> vecCmp n a pa.cmp x y True
+  , lt = \ (x : Vec a n) -> \ (y : Vec a n) -> vecCmp n a pa.cmp x y False
   };
 
 PCmpSeq : (n : Num) -> (a : isort 0) -> PCmp a -> PCmp (seq n a);
@@ -725,7 +726,7 @@ PCmpSeq n =
            (\ (a:isort 0) (pa : PCmp a) -> error (PCmp (Stream a)) "invalid Cmp instance")
            n;
 
-PCmpWord : (n : Nat) -> PCmp (Vec n Bool);
+PCmpWord : (n : Nat) -> PCmp (Vec Bool n);
 PCmpWord n = { cmpEq = PEqWord n, cmp = bvCmp n, le = bvule n, lt = bvult n };
 
 PCmpSeqBool : (n : Num) -> PCmp (seq n Bool);
@@ -823,12 +824,12 @@ PSignedCmp a =
     , slt : a -> a -> Bool
     };
 
-PSignedCmpVec : (n : Nat) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (Vec n a);
+PSignedCmpVec : (n : Nat) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (Vec a n);
 PSignedCmpVec n a pa =
    { signedCmpEq = PEqVec n a pa.signedCmpEq
    , scmp = vecCmp n a pa.scmp
-   , sle = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.scmp x y True
-   , slt = \ (x : Vec n a) -> \ (y : Vec n a) -> vecCmp n a pa.scmp x y False
+   , sle = \ (x : Vec a n) -> \ (y : Vec a n) -> vecCmp n a pa.scmp x y True
+   , slt = \ (x : Vec a n) -> \ (y : Vec a n) -> vecCmp n a pa.scmp x y False
    };
 
 PSignedCmpSeq : (n : Num) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (seq n a);
@@ -838,7 +839,7 @@ PSignedCmpSeq n =
            (\ (a:isort 0) (pa : PSignedCmp a) -> error (PSignedCmp (Stream a)) "invalid SignedCmp instance")
            n;
 
-PSignedCmpWord : (n : Nat) -> PSignedCmp (Vec n Bool);
+PSignedCmpWord : (n : Nat) -> PSignedCmp (Vec Bool n);
 PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n, sle = bvsle n, slt = bvslt n };
 
 PSignedCmpSeqBool : (n : Num) -> PSignedCmp (seq n Bool);
@@ -981,7 +982,7 @@ PLogicBit =
   , not  = not
   };
 
-PLogicVec : (n : Nat) -> (a : isort 0) -> PLogic a -> PLogic (Vec n a);
+PLogicVec : (n : Nat) -> (a : isort 0) -> PLogic a -> PLogic (Vec a n);
 PLogicVec n a pa =
   { logicZero = replicate n a pa.logicZero
   , and  = zipWith a a a pa.and n
@@ -1006,7 +1007,7 @@ PLogicSeq n =
 	   (\ (a:isort 0) -> PLogicStream a)
 	   n;
 
-PLogicWord : (n : Nat) -> PLogic (Vec n Bool);
+PLogicWord : (n : Nat) -> PLogic (Vec Bool n);
 PLogicWord n =
   { logicZero = bvNat n 0
   , and  = bvAnd n
@@ -1113,7 +1114,7 @@ PRingRational =
   , int = integerToRational
   };
 
-PRingVec : (n : Nat) -> (a : isort 0) -> PRing a -> PRing (Vec n a);
+PRingVec : (n : Nat) -> (a : isort 0) -> PRing a -> PRing (Vec a n);
 PRingVec n a pa =
   { ringZero = replicate n a pa.ringZero
   , add = zipWith a a a pa.add n
@@ -1140,7 +1141,7 @@ PRingSeq n =
            (\ (a:isort 0) -> PRingStream a)
            n;
 
-PRingWord : (n : Nat) -> PRing (Vec n Bool);
+PRingWord : (n : Nat) -> PRing (Vec Bool n);
 PRingWord n =
   { ringZero = bvNat n 0
   , add = bvAdd n
@@ -1218,7 +1219,7 @@ PIntegral a =
    , posneg : a -> Either Nat Nat
    -- 'Left n' means non-negative, 'Right n' means negative.
    -- NOTE: 'posneg' could be computed from 'toInt', but keeping it
-   -- separate makes it possible to convert from e.g. 'Vec n Bool' to
+   -- separate makes it possible to convert from e.g. 'Vec Bool n' to
    -- 'Nat' without a symbolic comparison at type 'Integer'.
    };
 
@@ -1238,14 +1239,14 @@ PIntegralInteger =
 posNegCases : (a : sort 0) -> PIntegral a -> (r : sort 0) -> (Nat -> r) -> (Nat -> r) -> a -> r;
 posNegCases a p r pos neg x = either Nat Nat r pos neg (p.posneg x);
 
-PIntegralWord : (n : Nat) -> PIntegral (Vec n Bool);
+PIntegralWord : (n : Nat) -> PIntegral (Vec Bool n);
 PIntegralWord n =
    { integralRing = PRingWord n
    , div = bvUDiv n
    , mod = bvURem n
    , toInt = bvToInt n
    -- words are always considered non-negative
-   , posneg = \ (x : Vec n Bool) -> Left Nat Nat (bvToNat n x)
+   , posneg = \ (x : Vec Bool n) -> Left Nat Nat (bvToNat n x)
    };
 
 PIntegralSeqBool : (n : Num) -> PIntegral (seq n Bool);
@@ -1447,18 +1448,18 @@ ecLg2 n =
 ecSDiv : (n : Num) -> seq n Bool -> seq n Bool -> seq n Bool;
 ecSDiv n =
   Num#rec (\ (n:Num) -> seq n Bool -> seq n Bool -> seq n Bool)
-    (Nat__rec (\ (n:Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool)
-      (error (Vec 0 Bool -> Vec 0 Bool -> Vec 0 Bool) "ecSDiv: illegal 0-width word")
-      (\ (n':Nat) -> \ (_:Vec n' Bool -> Vec n' Bool -> Vec n' Bool) -> bvSDiv n'))
+    (Nat__rec (\ (n:Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n)
+      (error (Vec Bool 0 -> Vec Bool 0 -> Vec Bool 0) "ecSDiv: illegal 0-width word")
+      (\ (n':Nat) -> \ (_:Vec Bool n' -> Vec Bool n' -> Vec Bool n') -> bvSDiv n'))
     (error (Stream Bool -> Stream Bool -> Stream Bool) "ecSDiv: expected finite word")
     n;
 
 ecSMod : (n : Num) -> seq n Bool -> seq n Bool -> seq n Bool;
 ecSMod n =
   Num#rec (\ (n:Num) -> seq n Bool -> seq n Bool -> seq n Bool)
-    (Nat__rec (\ (n:Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool)
-      (error (Vec 0 Bool -> Vec 0 Bool -> Vec 0 Bool) "ecSMod: illegal 0-width word")
-      (\ (n':Nat) -> \ (_:Vec n' Bool -> Vec n' Bool -> Vec n' Bool) -> bvSRem n'))
+    (Nat__rec (\ (n:Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n)
+      (error (Vec Bool 0 -> Vec Bool 0 -> Vec Bool 0) "ecSMod: illegal 0-width word")
+      (\ (n':Nat) -> \ (_:Vec Bool n' -> Vec Bool n' -> Vec Bool n') -> bvSRem n'))
     (error (Stream Bool -> Stream Bool -> Stream Bool) "ecSMod: expected finite word")
     n;
 
@@ -1538,8 +1539,8 @@ ecShiftL m =
     (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> seq m a -> ix -> seq m a)
 
     -- Case for (TCNum m)
-    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
-        posNegCases ix pix (Vec m a)
+    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec a m) ->
+        posNegCases ix pix (Vec a m)
           (shiftL m a (ecZero a pz) xs)
           (shiftR m a (ecZero a pz) xs))
 
@@ -1558,8 +1559,8 @@ ecShiftR m =
     (\ (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> seq m a -> ix -> seq m a)
 
     -- Case for (TCNum m)
-    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
-        posNegCases ix pix (Vec m a)
+    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec a m) ->
+        posNegCases ix pix (Vec a m)
           (shiftR m a (ecZero a pz) xs)
           (shiftL m a (ecZero a pz) xs))
 
@@ -1577,10 +1578,10 @@ ecSShiftR =
     (\ (n:Nat) ->
          (\ (ix : sort 0) -> \ (pix : PIntegral ix) ->
             natCase
-              (\ (w : Nat) -> Vec w Bool -> ix -> Vec w Bool)
-              (\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs)
-              (\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) ->
-                   posNegCases ix pix (Vec (Succ w) Bool)
+              (\ (w : Nat) -> Vec Bool w -> ix -> Vec Bool w)
+              (\ (xs : Vec Bool 0) -> \ (_ : ix) -> xs)
+              (\ (w : Nat) -> \ (xs : Vec Bool (Succ w)) ->
+                   posNegCases ix pix (Vec Bool (Succ w))
                      (bvSShr w xs)
                      (bvShl (Succ w) xs))
               n));
@@ -1589,8 +1590,8 @@ ecRotL : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m
 ecRotL =
   finNumRec
     (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a)
-    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
-      posNegCases ix pix (Vec m a)
+    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec a m) ->
+      posNegCases ix pix (Vec a m)
         (rotateL m a xs)
         (rotateR m a xs));
 
@@ -1598,8 +1599,8 @@ ecRotR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m
 ecRotR =
   finNumRec
     (\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a)
-    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
-      posNegCases ix pix (Vec m a)
+    (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec a m) ->
+      posNegCases ix pix (Vec a m)
         (rotateR m a xs)
         (rotateL m a xs));
 
@@ -1610,7 +1611,7 @@ ecCat =
        seq (tcAdd m n) a)
     (\ (m:Nat) ->
        Num_rec
-         (\ (n:Num) -> (a:isort 0) -> Vec m a -> seq n a ->
+         (\ (n:Num) -> (a:isort 0) -> Vec a m -> seq n a ->
             seq (tcAdd (TCNum m) n) a)
          -- Case for (TCNum m, TCNum n)
          (\ (n:Nat) -> \ (a:isort 0) -> append m n a)
@@ -1624,9 +1625,9 @@ ecTake =
 
     (\ (m:Nat) ->
        Num_rec
-         (\ (n:Num) -> (a:isort 0) -> seq (tcAdd (TCNum m) n) a -> Vec m a)
+         (\ (n:Num) -> (a:isort 0) -> seq (tcAdd (TCNum m) n) a -> Vec a m)
          -- The case (TCNum m, TCNum n)
-         (\ (n:Nat) -> \ (a:isort 0) -> \ (xs: Vec (addNat m n) a) -> take a m n xs)
+         (\ (n:Nat) -> \ (a:isort 0) -> \ (xs: Vec a (addNat m n)) -> take a m n xs)
          -- The case (TCNum m, infinity)
          (\ (a:isort 0) -> \ (xs: Stream a) -> streamTake a m xs))
 
@@ -1645,7 +1646,7 @@ ecDrop =
        Num_rec
          (\ (n:Num) -> (a:isort 0) -> seq (tcAdd (TCNum m) n) a -> seq n a)
          -- The case (TCNum n, TCNum m)
-         (\ (n:Nat) -> \ (a:isort 0) -> \ (xs: Vec (addNat m n) a) -> drop a m n xs)
+         (\ (n:Nat) -> \ (a:isort 0) -> \ (xs: Vec a (addNat m n)) -> drop a m n xs)
          -- The case (TCNum m, infinity)
          (\ (a:isort 0) -> \ (xs: Stream a) -> streamDrop a m xs));
 
@@ -1656,7 +1657,7 @@ ecJoin m =
        seq (tcMul m n) a)
     (\ (m:Nat) ->
        finNumRec
-         (\ (n:Num) -> (a:isort 0) -> Vec m (seq n a) ->
+         (\ (n:Num) -> (a:isort 0) -> Vec (seq n a) m ->
             seq (tcMul (TCNum m) n) a)
          -- Case for (TCNum m, TCNum n)
          (\ (n:Nat) -> \ (a:isort 0) -> join m n a))
@@ -1667,10 +1668,10 @@ ecJoin m =
        -- Case for (TCInf, TCNum n)
        (\ (n:Nat) -> \ (a:isort 0) ->
           natCase
-            (\ (n':Nat) -> Stream (Vec n' a) ->
+            (\ (n':Nat) -> Stream (Vec a n') ->
                seq (if0Nat Num n' (TCNum 0) TCInf) a)
-            (\ (s:Stream (Vec 0 a)) -> EmptyVec a)
-            (\ (n':Nat) -> \ (s:Stream (Vec (Succ n') a)) ->
+            (\ (s:Stream (Vec a 0)) -> EmptyVec a)
+            (\ (n':Nat) -> \ (s:Stream (Vec a (Succ n'))) ->
                streamJoin a n' s)
             n))
        -- No case for (TCInf, TCInf), shouldn't happen
@@ -1685,7 +1686,7 @@ ecSplit m =
     (\ (m:Nat) ->
        finNumRec
          (\ (n:Num) -> (a:isort 0) -> seq (tcMul (TCNum m) n) a ->
-            Vec m (seq n a))
+            Vec (seq n a) m)
          -- Case for (TCNum m, TCNum n)
          (\ (n:Nat) -> \ (a:isort 0) -> split m n a))
          -- No case for (TCNum m, TCInf), shouldn't happen
@@ -1697,8 +1698,8 @@ ecSplit m =
           natCase
             (\ (n':Nat) ->
                seq (if0Nat Num n' (TCNum 0) TCInf) a ->
-               Stream (Vec n' a))
-            (streamConst (Vec 0 a))
+               Stream (Vec a n'))
+            (streamConst (Vec a 0))
             (\ (n':Nat) -> streamSplit a (Succ n'))
             n))
        -- No case for (TCInf, TCInf), shouldn't happen
@@ -1716,20 +1717,20 @@ ecTranspose m n a =
     (\ (m : Num) -> seq m (seq n a) -> seq n (seq m a))
     (\ (m : Nat) ->
       Num#rec
-        (\ (n : Num) -> Vec m (seq n a) -> seq n (Vec m a))
+        (\ (n : Num) -> Vec (seq n a) m -> seq n (Vec a m))
         (\ (n : Nat) -> transpose m n a)
-        (\ (xss : Vec m (Stream a)) ->
-          MkStream (Vec m a) (\ (i : Nat) ->
+        (\ (xss : Vec (Stream a) m) ->
+          MkStream (Vec a m) (\ (i : Nat) ->
             gen m a (\ (j : Nat) ->
               streamGet a (at m (Stream a) xss j) i)))
         n
     )
     ( Num#rec
         (\ (n : Num) -> Stream (seq n a) -> seq n (Stream a))
-        (\ (n : Nat) -> \ (xss : Stream (Vec n a)) ->
+        (\ (n : Nat) -> \ (xss : Stream (Vec a n)) ->
           gen n (Stream a) (\ (i : Nat) ->
             MkStream a (\ (j : Nat) ->
-              at n a (streamGet (Vec n a) xss j) i)))
+              at n a (streamGet (Vec a n) xss j) i)))
         (\ (xss : Stream (Stream a)) ->
           MkStream (Stream a) (\ (i : Nat) ->
             MkStream a (\ (j : Nat) ->
@@ -1742,7 +1743,7 @@ ecAt : (n : Num) -> (a : isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a ->
 ecAt n =
   Num#rec1
     (\ (n:Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a)
-    (\ (n:Nat) -> \ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
+    (\ (n:Nat) -> \ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec a n) ->
           posNegCases ix pix a
             (at n a xs)
             (\ (_:Nat) -> at n a xs 0))
@@ -1900,21 +1901,21 @@ ecInfFromThen a pa x y =
 
 
 -- Run-time error
-ecError : (a : isort 0) -> (len : Num) -> seq len (Vec 8 Bool) -> a;
+ecError : (a : isort 0) -> (len : Num) -> seq len (Vec Bool 8) -> a;
 ecError a =
   finNumRec
-    (\ (len:Num) -> seq len (Vec 8 Bool) -> a)
-    (\ (len:Nat) (msg:Vec len (Vec 8 Bool)) ->
+    (\ (len:Num) -> seq len (Vec Bool 8) -> a)
+    (\ (len:Nat) (msg:Vec (Vec Bool 8) len) ->
        error a (appendString "encountered call to the Cryptol 'error' function: "
                              (bytesToString len msg))
     );
 
 -- Random values
-ecRandom : (a : isort 0) -> Vec 256 Bool -> a;
+ecRandom : (a : isort 0) -> Vec Bool 256 -> a;
 ecRandom a _ = error a "Cryptol.random";
 
 -- Trace function; simply return the final argument
-ecTrace : (n : Num) -> (a b : sort 0) -> seq n (Vec 8 Bool) -> a -> b -> b;
+ecTrace : (n : Num) -> (a b : sort 0) -> seq n (Vec Bool 8) -> a -> b -> b;
 ecTrace _ _ _ _ _ x = x;
 
 
@@ -1932,7 +1933,7 @@ ecDeepseq a b pa x y = y;
 ecParmap : (a:isort 0) -> (b:isort 0) -> (n: Num) -> PEq b -> (a -> b) -> seq n a -> seq n b;
 ecParmap a b n pb =
   Num#rec (\ (n:Num) -> (a -> b) -> seq n a -> seq n b)
-    ( \ (n:Nat) -> \ (f: a -> b) -> \ (xs: Vec n a) -> map a b f n xs )
+    ( \ (n:Nat) -> \ (f: a -> b) -> \ (xs: Vec a n) -> map a b f n xs )
     ( \ (f: a -> b) -> \ (xs:Stream a) -> error (Stream b) "Unexpected infinite stream in parmap" )
     n;
 
@@ -1940,7 +1941,7 @@ ecParmap a b n pb =
 ecFoldl : (n : Num) -> (a : sort 0) -> (b : isort 0) -> (a -> b -> a) -> a -> seq n b -> a;
 ecFoldl n a b f z =
   Num#rec (\ (n : Num) -> seq n b -> a)
-    (\ (n : Nat) -> \ (xs : Vec n b) -> foldl b a n f z xs)
+    (\ (n : Nat) -> \ (xs : Vec b n) -> foldl b a n f z xs)
     (\ (xs : Stream b) -> error a "Unexpected infinite stream in foldl" )
     n;
 
@@ -1954,7 +1955,7 @@ ecScanl :
   (n : Num) -> (a : sort 0) -> (b : sort 0) -> (a -> b -> a) -> a -> seq n b -> seq (tcAdd (TCNum 1) n) a;
 ecScanl n a b f z =
   Num#rec (\ (n : Num) -> seq n b -> seq (tcAdd (TCNum 1) n) a)
-    (\ (n:Nat) -> \ (xs : Vec n b) -> scanl b a n f z xs)
+    (\ (n:Nat) -> \ (xs : Vec b n) -> scanl b a n f z xs)
     (\ (xs : Stream b) -> streamScanl b a f z xs)
     n;
 
@@ -2027,22 +2028,22 @@ ecFpToBits e p _ = error (seq (tcAdd e p) Bool) "Unimplemented: fpToBits";
 ecFpEq : (e : Num) -> (p : Num) -> TCFloat e p -> TCFloat e p -> Bool;
 ecFpEq e p _ _ = error Bool "Unimplemented: =.=";
 
-ecFpAdd : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpAdd : (e : Num) -> (p : Num) -> Vec Bool 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpAdd e p _ _ _ = error (TCFloat e p) "Unimplemented: fpAdd";
 
-ecFpSub : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpSub : (e : Num) -> (p : Num) -> Vec Bool 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpSub e p _ _ _ = error (TCFloat e p) "Unimplemented: fpSub";
 
-ecFpMul : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpMul : (e : Num) -> (p : Num) -> Vec Bool 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpMul e p _ _ _ = error (TCFloat e p) "Unimplemented: fpMul";
 
-ecFpDiv : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p -> TCFloat e p;
+ecFpDiv : (e : Num) -> (p : Num) -> Vec Bool 3 -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 ecFpDiv e p _ _ _ = error (TCFloat e p) "Unimplemented: fpDiv";
 
 ecFpToRational : (e : Num) -> (p : Num) -> TCFloat e p -> Rational;
 ecFpToRational e p _ = error Rational "Unimplemented: fpToRational";
 
-ecFpFromRational : (e : Num) -> (p : Num) -> Vec 3 Bool -> Rational -> TCFloat e p;
+ecFpFromRational : (e : Num) -> (p : Num) -> Vec Bool 3 -> Rational -> TCFloat e p;
 ecFpFromRational e p _ _ = error (TCFloat e p) "Unimplemented: fpFromRational";
 
 fpIsNaN : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
@@ -2064,14 +2065,14 @@ fpIsSubnormal : (e : Num) -> (p : Num) -> TCFloat e p -> Bool;
 fpIsSubnormal e p x = error Bool "Unimplemented: fpIsSubnormal";
 
 fpFMA :
-  (e : Num) -> (p : Num) -> Vec 3 Bool ->
+  (e : Num) -> (p : Num) -> Vec Bool 3 ->
   TCFloat e p -> TCFloat e p -> TCFloat e p -> TCFloat e p;
 fpFMA e p r x y z = error (TCFloat e p) "Unimplemented: fpFMA";
 
 fpAbs : (e : Num) -> (p : Num) -> TCFloat e p -> TCFloat e p;
 fpAbs e p x = error (TCFloat e p) "Unimplemented: fpAbs";
 
-fpSqrt : (e : Num) -> (p : Num) -> Vec 3 Bool -> TCFloat e p -> TCFloat e p;
+fpSqrt : (e : Num) -> (p : Num) -> Vec Bool 3 -> TCFloat e p -> TCFloat e p;
 fpSqrt e p r x = error (TCFloat e p) "Unimplemented: fpSqrt";
 
 
@@ -2083,12 +2084,12 @@ ecUpdate : (n : Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -
 ecUpdate n =
   Num#rec1
     (\ (n:Num) -> (a:isort 0) -> (ix : sort 0) -> PIntegral ix -> seq n a -> ix -> a -> seq n a)
-    (\ (n:Nat) -> \ (a:isort 0) -> \ (ix : sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Vec n a) ->
+    (\ (n:Nat) -> \ (a:isort 0) -> \ (ix : sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Vec a n) ->
        -- Case for (TCNum n, TCNum w)
-       posNegCases ix pix (a -> Vec n a)
+       posNegCases ix pix (a -> Vec a n)
          (upd n a xs)
          (\ (_:Nat) -> \ (_:a) -> xs))
-         -- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
+         -- (error (Nat -> a -> Vec a n) "ecUpdate: negative index"))
     (\ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Stream a) ->
        posNegCases ix pix (a -> Stream a)
          (streamUpd a xs)
@@ -2101,11 +2102,11 @@ ecUpdateEnd : (n : Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n
 ecUpdateEnd =
   finNumRec
     (\ (n:Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a -> seq n a)
-    (\ (n:Nat) -> \ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
-       posNegCases ix pix (a -> Vec n a)
+    (\ (n:Nat) -> \ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec a n) ->
+       posNegCases ix pix (a -> Vec a n)
          (\ (i:Nat) -> upd n a xs (subNat (subNat n 1) i))
          (\ (_:Nat) -> \ (_:a) -> xs));
-         -- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"))
+         -- (error (Nat -> a -> Vec a n) "ecUpdateEnd: negative index"))
     -- No TCInf case, shouldn't happen
 
 
@@ -2129,8 +2130,8 @@ ecSExt =
     (\ (m n : Num) -> seq n Bool -> seq (tcAdd m n) Bool)
     (\ (m n : Nat) ->
        natCase
-         (\ (n' : Nat) -> Vec n' Bool -> Vec (addNat m n') Bool)
-         (\ (_ : Vec 0 Bool) -> bvNat (addNat m 0) 0)
+         (\ (n' : Nat) -> Vec Bool n' -> Vec Bool (addNat m n'))
+         (\ (_ : Vec Bool 0) -> bvNat (addNat m 0) 0)
          (bvSExt m)
          n);
 
@@ -2168,7 +2169,7 @@ ecArrayCopy : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool ->
 ecArrayCopy = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> Array (seq n Bool) a -> seq n Bool -> seq n Bool -> Array (seq n Bool) a) arrayCopy;
 
 ecArrayEq : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> Array (seq n Bool) a -> Bool;
-ecArrayEq = finNumRec (\ (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> Array (seq n Bool) a -> Bool) (\ (n:Nat) -> arrayEq (Vec n Bool));
+ecArrayEq = finNumRec (\ (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> Array (seq n Bool) a -> Bool) (\ (n:Nat) -> arrayEq (Vec Bool n));
 
 ecArraySet : (n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a;
 ecArraySet = finNumRec (\(n : Num) -> (a : sort 0) -> Array (seq n Bool) a -> seq n Bool -> a -> seq n Bool -> Array (seq n Bool) a) arraySet;
@@ -2202,8 +2203,8 @@ ecPmult =
    seq (tcAdd (TCNum 1) (tcAdd u v)) Bool
   )
   (\ (u v : Nat) ->
-   \ (x : Vec (addNat 1 u) Bool) ->
-   \ (y : Vec (addNat 1 v) Bool) ->
+   \ (x : Vec Bool (addNat 1 u)) ->
+   \ (y : Vec Bool (addNat 1 v)) ->
    coerceVec Bool (Succ (addNat u v)) (addNat 1 (addNat u v))
    (sym Nat (addNat 1 (addNat u v)) (Succ (addNat u v)) (addNat_1 (addNat u v)))
    (polyMul u v
@@ -2225,57 +2226,57 @@ ecPmod =
    seq v Bool
   )
   (\ (u v : Nat) ->
-   \ (x : Vec u Bool) ->
-   \ (y : Vec (addNat 1 v) Bool) ->
+   \ (x : Vec Bool u) ->
+   \ (y : Vec Bool (addNat 1 v)) ->
    polyMod u v x (coerceVec Bool (addNat 1 v) (Succ v) (addNat_1 v) y)
   );
 
 --------------------------------------------------------------------------------
 -- Suite-B Primitives
 
-AESEncRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
+AESEncRound : Vec (Vec Bool 32) 4 -> Vec (Vec Bool 32) 4;
 AESEncRound x =
-  error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESEncRound";
+  error (Vec (Vec Bool 32) 4) "Unimplemented: AESEncRound";
 
-AESEncFinalRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
+AESEncFinalRound : Vec (Vec Bool 32) 4 -> Vec (Vec Bool 32) 4;
 AESEncFinalRound x =
-  error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESEncFinalRound";
+  error (Vec (Vec Bool 32) 4) "Unimplemented: AESEncFinalRound";
 
-AESDecRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
+AESDecRound : Vec (Vec Bool 32) 4 -> Vec (Vec Bool 32) 4;
 AESDecRound x =
-  error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESDecRound";
+  error (Vec (Vec Bool 32) 4) "Unimplemented: AESDecRound";
 
-AESDecFinalRound : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
+AESDecFinalRound : Vec (Vec Bool 32) 4 -> Vec (Vec Bool 32) 4;
 AESDecFinalRound x =
-  error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESDecFinalRound";
+  error (Vec (Vec Bool 32) 4) "Unimplemented: AESDecFinalRound";
 
-AESInvMixColumns : Vec 4 (Vec 32 Bool) -> Vec 4 (Vec 32 Bool);
+AESInvMixColumns : Vec (Vec Bool 32) 4 -> Vec (Vec Bool 32) 4;
 AESInvMixColumns x =
-  error (Vec 4 (Vec 32 Bool)) "Unimplemented: AESInvMixColumns";
+  error (Vec (Vec Bool 32) 4) "Unimplemented: AESInvMixColumns";
 
 AESKeyExpand :
   (k : Num) ->
-  seq k (Vec 32 Bool) ->
-  seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool);
+  seq k (Vec Bool 32) ->
+  seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec Bool 32);
 AESKeyExpand k x =
-  error (seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec 32 Bool))
+  error (seq (tcMul (TCNum 4) (tcAdd (TCNum 7) k)) (Vec Bool 32))
     "Unimplemented: AESKeyExpand";
 
-processSHA2_224 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 7 (Vec 32 Bool);
+processSHA2_224 : (n : Num) -> seq n (Vec (Vec Bool 32) 16) -> Vec (Vec Bool 32) 7;
 processSHA2_224 n x =
-  error (Vec 7 (Vec 32 Bool)) "Unimplemented: processSHA2_224";
+  error (Vec (Vec Bool 32) 7) "Unimplemented: processSHA2_224";
 
-processSHA2_256 : (n : Num) -> seq n (Vec 16 (Vec 32 Bool)) -> Vec 8 (Vec 32 Bool);
+processSHA2_256 : (n : Num) -> seq n (Vec (Vec Bool 32) 16) -> Vec (Vec Bool 32) 8;
 processSHA2_256 n x =
-  error (Vec 8 (Vec 32 Bool)) "Unimplemented: processSHA2_256";
+  error (Vec (Vec Bool 32) 8) "Unimplemented: processSHA2_256";
 
-processSHA2_384 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 6 (Vec 64 Bool);
+processSHA2_384 : (n : Num) -> seq n (Vec (Vec Bool 64) 16) -> Vec (Vec Bool 64) 6;
 processSHA2_384 n x =
-  error (Vec 6 (Vec 64 Bool)) "Unimplemented: processSHA2_384";
+  error (Vec (Vec Bool 64) 6) "Unimplemented: processSHA2_384";
 
-processSHA2_512 : (n : Num) -> seq n (Vec 16 (Vec 64 Bool)) -> Vec 8 (Vec 64 Bool);
+processSHA2_512 : (n : Num) -> seq n (Vec (Vec Bool 64) 16) -> Vec (Vec Bool 64) 8;
 processSHA2_512 n x =
-  error (Vec 8 (Vec 64 Bool)) "Unimplemented: processSHA2_512";
+  error (Vec (Vec Bool 64) 8) "Unimplemented: processSHA2_512";
 
 --------------------------------------------------------------------------------
 -- Prime-EC Primitives
@@ -2307,7 +2308,7 @@ ec_twin_mult p x y z =
 --------------------------------------------------------------------------------
 -- Rewrite rules
 
-axiom replicate_False : (n : Nat) -> Eq (Vec n Bool) (replicate n Bool False) (bvNat n 0);
+axiom replicate_False : (n : Nat) -> Eq (Vec Bool n) (replicate n Bool False) (bvNat n 0);
 
 axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;
 
@@ -2315,7 +2316,7 @@ axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;
 axiom demote_add_distr
   : (w : Nat)
   -> (x y : Num)
-  -> Eq (Vec w Bool)
+  -> Eq (Vec Bool w)
         (ecNumber (tcAdd x y) (TCNum w))
         (bvAdd w (ecNumber x (TCNum w)) (ecNumber y (TCNum w)));
 -}
diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
index 9dbdbdea87..dffbdc6b5c 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
@@ -1331,7 +1331,7 @@ importExpr sc expr =
                 -- of type `seq (TCNum 2) a`.
                if | Just (n, a) <- asSeqType t ->
                       return (n, a)
-                  | Just (n, a) <- asVectorType t -> do
+                  | Just (a, n) <- asVectorType t -> do
                       n' <- scGlobalApply sc "Cryptol.TCNum" [n]
                       return (n', a)
                   | otherwise -> do
diff --git a/otherTests/saw-core/Tests/Rewriter.hs b/otherTests/saw-core/Tests/Rewriter.hs
index 6453cd2485..8e53e2eed8 100644
--- a/otherTests/saw-core/Tests/Rewriter.hs
+++ b/otherTests/saw-core/Tests/Rewriter.hs
@@ -41,7 +41,7 @@ prelude_bveq_sameL_test =
     natType <- scNatType sc
     n <- scFreshVariable sc "n" natType
     boolType <- scBoolType sc
-    bvType <- scVecType sc n boolType
+    bvType <- scVecType sc boolType n
     x <- scFreshVariable sc "x" bvType
     z <- scFreshVariable sc "z" bvType
     let lhs =
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs b/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs
index fc9f745baa..e3846726b8 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs
@@ -215,7 +215,7 @@ mkSizeArg tyArgTerm = do
   openToSetupTerm $
     OT.applyGlobal "Cryptol.ecNumber"
       [ OT.term tyArgTerm
-      , OT.vectorType sizeBitSize OT.boolType
+      , OT.vectorType OT.boolType sizeBitSize
       , OT.applyGlobal "Cryptol.PLiteralSeqBool"
           [OT.applyGlobal "Cryptol.TCNum" [sizeBitSize]]
       ]
@@ -491,7 +491,7 @@ arrayTypeInfo tenv lenTypes ffiBasicType = do
   FFITypeInfo {..} <- basicTypeInfo ffiBasicType
   pure FFITypeInfo
     { ffiLLVMType = llvm_array totalLen ffiLLVMType
-    , ffiLLVMCoreType = OT.vectorType totalLenTerm ffiLLVMCoreType
+    , ffiLLVMCoreType = OT.vectorType ffiLLVMCoreType totalLenTerm
     , ffiConv =
         case (lenTerms, ffiConv) of
           -- If the array is flat and there is no need to convert individual
@@ -502,7 +502,7 @@ arrayTypeInfo tenv lenTypes ffiBasicType = do
                 basicToLLVM = maybe (Just id) ffiToLLVM ffiConv
                 cumulLenTerms = map OT.nat $ scanl1 (*) lens
                 arrCryType :| cumulElemTypes =
-                  NE.scanr OT.vectorType basicCryType lenTerms
+                  NE.scanr (flip OT.vectorType) basicCryType lenTerms
 
                 noArrayLengths :: a
                 noArrayLengths =
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs
index e44fc91eb2..4abe01823b 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs
@@ -1365,7 +1365,7 @@ typeToSC sc t =
     Crucible.Array sz ty ->
       do n <- scNat sc (fromIntegral sz)
          ty' <- typeToSC sc ty
-         scVecType sc n ty'
+         scVecType sc ty' n
     Crucible.Struct fields ->
       do fields' <- V.toList <$> traverse (typeToSC sc . view Crucible.fieldVal) fields
          scTupleType sc fields'
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
index 29370bf813..b143a40227 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
@@ -2092,7 +2092,7 @@ setupArg sc cc ecRef mty0 tp0 =
               (eltCty, eltScTp) <- typeShapeToSAWTypes eltShp
               arraySzTerm <- scNat sc $ fromIntegral @Int @Natural arraySz
               let cty = Cryptol.tSeq (Cryptol.tNum (toInteger @Int arraySz)) eltCty
-              scTp <- scVecType sc arraySzTerm eltScTp
+              scTp <- scVecType sc eltScTp arraySzTerm
               pure (cty, scTp)
 
             StructShape mty _ ->
@@ -2152,7 +2152,7 @@ setupArg sc cc ecRef mty0 tp0 =
             PrimShape {} ->
               termToRegValue sym (shapeType shp) t
             ArrayShape _ _ eltSz eltShp len -> do
-              (arraySz :*: eltScTp) <-
+              (eltScTp :*: arraySz) <-
                 case asVecType scTp of
                   Just nt -> pure nt
                   Nothing -> do
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs b/saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs
index 0fef1da95d..49f7524c01 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs
@@ -486,7 +486,7 @@ shapeToTerm' sc = go
     mkVec n ty =
       do
         n' <- SAW.scNat sc (fromIntegral n)
-        SAW.scVecType sc n' ty
+        SAW.scVecType sc ty n'
 
     goAgElem :: CryTermAdaptor Integer -> AgElemShape -> m SAW.Term
     goAgElem ada (AgElemShape _ _ shp) = go ada shp
diff --git a/saw-central/src/SAWCentral/Yosys/State.hs b/saw-central/src/SAWCentral/Yosys/State.hs
index 807468363e..d9c0485808 100644
--- a/saw-central/src/SAWCentral/Yosys/State.hs
+++ b/saw-central/src/SAWCentral/Yosys/State.hs
@@ -198,12 +198,12 @@ composeYosysSequentialHelper sc s n =
      width <- SC.scNat sc $ fromIntegral n
      extendedInputFields <-
        forM (s ^. yosysSequentialInputFields) $ \(ty, cty) ->
-       do exty <- SC.scVecType sc width ty
+       do exty <- SC.scVecType sc ty width
           let excty = C.tSeq (C.tNum n) cty
           pure (exty, excty)
      extendedOutputFields <-
        forM (s ^. yosysSequentialOutputFields) $ \(ty, cty) ->
-       do exty <- SC.scVecType sc width ty
+       do exty <- SC.scVecType sc ty width
           let excty = C.tSeq (C.tNum n) cty
           pure (exty, excty)
      extendedInputType <- fieldsToType sc extendedInputFields
diff --git a/saw-central/src/SAWCentral/Yosys/Utils.hs b/saw-central/src/SAWCentral/Yosys/Utils.hs
index 82f680c835..0aaae1d040 100644
--- a/saw-central/src/SAWCentral/Yosys/Utils.hs
+++ b/saw-central/src/SAWCentral/Yosys/Utils.hs
@@ -399,7 +399,7 @@ scPreterms sc preterms = snd <$> go preterms
            -- Use `join` to concatenate same-length preterms
            do i' <- SC.scNat sc i
               boolty <- SC.scBoolType sc
-              ety <- SC.scVecType sc i' boolty
+              ety <- SC.scVecType sc boolty i'
               ps1' <- traverse (scPreterm sc) ps1
               v <- SC.scVector sc ety (p' : ps1')
               let len = List.genericLength ps1 + 1 :: Natural
diff --git a/saw-core-what4/src/SAWCoreWhat4/Common.hs b/saw-core-what4/src/SAWCoreWhat4/Common.hs
index bbe8a86f2d..5513524c2b 100644
--- a/saw-core-what4/src/SAWCoreWhat4/Common.hs
+++ b/saw-core-what4/src/SAWCoreWhat4/Common.hs
@@ -113,7 +113,7 @@ termOfTValue sc val =
     VVecType n a ->
       do n' <- scNat sc n
          a' <- termOfTValue sc a
-         scVecType sc n' a'
+         scVecType sc a' n'
     VDataType (ModuleIdentifier "Prelude.UnitType") [] []
       -> scUnitType sc
     VDataType (ModuleIdentifier "Prelude.PairType") [TValue a, TValue b] []
diff --git a/saw-core-what4/src/SAWCoreWhat4/ReturnTrip.hs b/saw-core-what4/src/SAWCoreWhat4/ReturnTrip.hs
index 89a3ea0d9d..d17f76fdc3 100644
--- a/saw-core-what4/src/SAWCoreWhat4/ReturnTrip.hs
+++ b/saw-core-what4/src/SAWCoreWhat4/ReturnTrip.hs
@@ -640,7 +640,8 @@ evaluateExpr sym st sc cache = f Map.empty
           case B.bvarType bvar of
             BaseBVRepr wrepr -> do
               w <- SC.scNat sc $ natValue wrepr
-              ty <- SC.scVecType sc w =<< SC.scBoolType sc
+              boolty <- SC.scBoolType sc
+              ty <- SC.scVecType sc boolty w
               x <- SC.scFreshVariable sc nm ty
               SAWExpr <$>
                 (SC.scBvForall sc w
diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
index 2054ad3ac9..22878151e3 100644
--- a/saw-core/prelude/Prelude.sawcore
+++ b/saw-core/prelude/Prelude.sawcore
@@ -1526,200 +1526,200 @@ Nat_complete_induction p f n0 =
 
 
 --------------------------------------------------------------------------------
--- "Vec n a" is an array of n elements, each with type "a".
-primitive Vec : Nat -> sort 0 -> sort 0;
+-- "Vec a n" is an array of n elements, each with type "a".
+primitive Vec : sort 0 -> Nat -> sort 0;
 
 -- Primitive function for generating an array.
-primitive gen : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec n a;
+primitive gen : (n : Nat) -> (a : sort 0) -> (Nat -> a) -> Vec a n;
 
 -- Primitive eliminators for arrays
-primitive head : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> a;
-primitive tail : (n : Nat) -> (a : sort 0) -> Vec (Succ n) a -> Vec n a;
+primitive head : (n : Nat) -> (a : sort 0) -> Vec a (Succ n) -> a;
+primitive tail : (n : Nat) -> (a : sort 0) -> Vec a (Succ n) -> Vec a n;
 
 -- Axioms describing head and tail in terms of gen
 axiom head_gen : (n : Nat) -> (a : sort 0) -> (f : Nat -> a) ->
                  Eq a (head n a (gen (Succ n) a f)) (f 0);
 
 axiom tail_gen : (n : Nat) -> (a : sort 0) -> (f : Nat -> a) ->
-                 Eq (Vec n a) (tail n a (gen (Succ n) a f))
+                 Eq (Vec a n) (tail n a (gen (Succ n) a f))
                               (gen n a (\ (i:Nat) -> f (Succ i)));
 
 -- An implementation for atWithDefault
 --
 -- FIXME: can we replace atWithDefault with this implementation? Or does some
 -- automation rely on atWithDefault being a primitive?
-atWithDefault' : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;
+atWithDefault' : (n : Nat) -> (a : sort 0) -> a -> Vec a n -> Nat -> a;
 atWithDefault' n_top a d =
   Nat__rec
-    (\ (n:Nat) -> Vec n a -> Nat -> a)
-    (\ (_:Vec 0 a) (_:Nat) -> d)
-    (\ (n:Nat) (rec_f: Vec n a -> Nat -> a) (v:Vec (Succ n) a) (i:Nat) ->
+    (\ (n:Nat) -> Vec a n -> Nat -> a)
+    (\ (_:Vec a 0) (_:Nat) -> d)
+    (\ (n:Nat) (rec_f: Vec a n -> Nat -> a) (v:Vec a (Succ n)) (i:Nat) ->
        Nat_cases a (head n a v)
                  (\ (i_prev:Nat) (_:a) -> rec_f (tail n a v) i_prev) i)
     n_top;
 
-primitive atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;
+primitive atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec a n -> Nat -> a;
 
-at : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a;
+at : (n : Nat) -> (a : isort 0) -> Vec a n -> Nat -> a;
 at n a v i = atWithDefault n a (error a "at: index out of bounds") v i;
 -- `at n a v i` has the precondition `ltNat i n`
 
-primitive EmptyVec : (a : sort 0) -> Vec 0 a;
+primitive EmptyVec : (a : sort 0) -> Vec a 0;
 
-ConsVec : (a : isort 0) -> a -> (n : Nat) -> Vec n a -> Vec (Succ n) a;
+ConsVec : (a : isort 0) -> a -> (n : Nat) -> Vec a n -> Vec a (Succ n);
 ConsVec a x n v =
   gen (Succ n) a (Nat_cases a x (\ (i:Nat) -> \ (a':a) -> at n a v i));
 
-upd : (n : Nat) -> (a : isort 0) -> Vec n a -> Nat -> a -> Vec n a;
+upd : (n : Nat) -> (a : isort 0) -> Vec a n -> Nat -> a -> Vec a n;
 upd n a v j x = gen n a (\ (i : Nat) -> ite a (equalNat i j) x (at n a v i));
 -- TODO: assertion that j < n
 
 -- | Defines a function that maps array elements from one range to another.
-map : (a : isort 0) -> (b : sort 0) -> (a -> b) -> (n : Nat) -> Vec n a -> Vec n b;
+map : (a : isort 0) -> (b : sort 0) -> (a -> b) -> (n : Nat) -> Vec a n -> Vec b n;
 map a b f n v = gen n b (\ (i : Nat) -> f (at n a v i));
 
 -- | Defines a function that maps array elements from one range to another.
 zipWith : (a b : isort 0) -> (c : sort 0)
         -> (a -> b -> c)
-        -> (n : Nat) -> Vec n a -> Vec n b -> Vec n c;
+        -> (n : Nat) -> Vec a n -> Vec b n -> Vec c n;
 zipWith a b c f n x y = gen n c (\ (i : Nat) -> f (at n a x i) (at n b y i));
 
 -- replicate n x returns an array with n copies of x.
-replicate : (n : Nat) -> (a : sort 0) -> a -> Vec n a;
+replicate : (n : Nat) -> (a : sort 0) -> a -> Vec a n;
 replicate n a x = gen n a (\ (_ : Nat) -> x);
 
 -- | Create a vector of length 1.
-single : (a : sort 0) -> a -> Vec 1 a;
+single : (a : sort 0) -> a -> Vec a 1;
 single = replicate 1;
 
 axiom at_single : (a : sort 0) -> (x : a) -> (i : Nat) -> Eq a (at 1 a (single a x) i) x;
 
 -- Zip together two lists (truncating the longer of the two).
-primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) #(a, b);
+primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec a m -> Vec b n -> Vec #(a, b) (minNat m n);
 
-primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -> b;
-primitive foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
-primitive scanl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> Vec (addNat 1 n) b;
+primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec a n -> b;
+primitive foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec a n -> b;
+primitive scanl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec a n -> Vec b (addNat 1 n);
 
 -- Axioms defining foldr
 axiom foldr_nil : (a b : sort 0) -> (f : a -> b -> b) -> (x : b) ->
-                  (v : Vec 0 a) -> Eq b (foldr a b 0 f x v) x;
+                  (v : Vec a 0) -> Eq b (foldr a b 0 f x v) x;
 axiom foldr_cons : (a b : sort 0) -> (n : Nat) -> (f : a -> b -> b) -> (x : b) ->
-                   (v : Vec (Succ n) a) ->
+                   (v : Vec a (Succ n)) ->
                    Eq b (foldr a b (Succ n) f x v)
                         (f (head n a v) (foldr a b n f x (tail n a v)));
 
 -- Axioms defining foldl
 axiom foldl_nil : (a b : sort 0) -> (f : b -> a -> b) -> (x : b) ->
-                  (v : Vec 0 a) -> Eq b (foldl a b 0 f x v) x;
+                  (v : Vec a 0) -> Eq b (foldl a b 0 f x v) x;
 axiom foldl_cons : (a b : sort 0) -> (n : Nat) -> (f : b -> a -> b) -> (x : b) ->
-                   (v : Vec (Succ n) a) ->
+                   (v : Vec a (Succ n)) ->
                    Eq b (foldl a b (Succ n) f x v)
                         (foldl a b n f (f x (head n a v)) (tail n a v));
 
-reverse : (n : Nat) -> (a : isort 0) -> Vec n a -> Vec n a;
+reverse : (n : Nat) -> (a : isort 0) -> Vec a n -> Vec a n;
 reverse n a xs = gen n a (\ (i : Nat) -> at n a xs (subNat (subNat n 1) i));
 
-transpose : (m n : Nat) -> (a : isort 0) -> Vec m (Vec n a) -> Vec n (Vec m a);
+transpose : (m n : Nat) -> (a : isort 0) -> Vec (Vec a n) m -> Vec (Vec a m) n;
 transpose m n a xss =
-  gen n (Vec m a) (\ (j : Nat) ->
-    gen m a (\ (i : Nat) -> at n a (at m (Vec n a) xss i) j));
+  gen n (Vec a m) (\ (j : Nat) ->
+    gen m a (\ (i : Nat) -> at n a (at m (Vec a n) xss i) j));
 
 -- | Return true if two vectors are equal, given a comparison function
 -- for elements.
 vecEq : (n : Nat) -> (a : isort 0) -> (a -> a -> Bool)
-      -> Vec n a -> Vec n a -> Bool;
+      -> Vec a n -> Vec a n -> Bool;
 vecEq n a eqFn x y =
   foldr Bool Bool n and True (zipWith a a Bool eqFn n x y);
 
 -- | Reflexivity axiom for 'vecEq'.
 axiom vecEq_refl : (n : Nat) -> (a : isort 0) -> (eqFn : a -> a -> Bool) ->
-                   ((x : a) -> Eq Bool (eqFn x x) True) -> (x : Vec n a) ->
+                   ((x : a) -> Eq Bool (eqFn x x) True) -> (x : Vec a n) ->
                    Eq Bool (vecEq n a eqFn x x) True;
 
 -- | Take a prefix of a vector.
-take : (a : isort 0) -> (m n : Nat) -> Vec (addNat m n) a -> Vec m a;
+take : (a : isort 0) -> (m n : Nat) -> Vec a (addNat m n) -> Vec a m;
 take a m n v = gen m a (\ (i : Nat) -> at (addNat m n) a v i);
 
 vecCong : (a : sort 0) -> (m n : Nat) -> Eq Nat m n ->
-           Eq (sort 0) (Vec m a) (Vec n a);
-vecCong a m n eq = eq_cong Nat m n eq (sort 0) (\ (i:Nat) -> Vec i a);
+           Eq (sort 0) (Vec a m) (Vec a n);
+vecCong a m n eq = eq_cong Nat m n eq (sort 0) (\ (i:Nat) -> Vec a i);
 
-coerceVec : (a : sort 0) -> (m n : Nat) -> Eq Nat m n -> Vec m a -> Vec n a;
-coerceVec a m n q = coerce (Vec m a) (Vec n a) (vecCong a m n q);
+coerceVec : (a : sort 0) -> (m n : Nat) -> Eq Nat m n -> Vec a m -> Vec a n;
+coerceVec a m n q = coerce (Vec a m) (Vec a n) (vecCong a m n q);
 
 -- | Simplify take  all elements from a vector.
 axiom take0 : (a : sort 0)
        -> (m : Nat)
-       -> (v : Vec (addNat m 0) a)
-       -> Eq (Vec m a)
+       -> (v : Vec a (addNat m 0))
+       -> Eq (Vec a m)
              (take a m 0 v)
              (coerceVec a (addNat m 0) m (eqNatAdd0 m) v);
 
 -- | Returns a suffix of a vector after a given number of elements.
-drop : (a : isort 0) -> (m n : Nat) -> Vec (addNat m n) a -> Vec n a;
+drop : (a : isort 0) -> (m n : Nat) -> Vec a (addNat m n) -> Vec a n;
 drop a m n v = gen n a (\ (i : Nat) -> at (addNat m n) a v (addNat m i));
 
 -- | Simplify drop 0-elements from a vector.
 axiom drop0 : (a : sort 0)
        -> (n : Nat)
-       -> (v : Vec (addNat 0 n) a)
-       -> Eq (Vec n a) (drop a 0 n v) v;
+       -> (v : Vec a (addNat 0 n))
+       -> Eq (Vec a n) (drop a 0 n v) v;
 
 -- | Select a range [i,..,i+n] of values from the array.
 slice : (a : isort 0)
       -> (m n o : Nat)
-      -> Vec (addNat (addNat m n) o) a -> Vec n a;
+      -> Vec a (addNat (addNat m n) o) -> Vec a n;
 slice a m n o v = drop a m n (take a (addNat m n) o v);
 
 -- Concatenate arrays together.
 join  : (m n : Nat)
        -> (a : isort 0)
-       -> Vec m (Vec n a)
-       -> Vec (mulNat m n) a;
+       -> Vec (Vec a n) m
+       -> Vec a (mulNat m n);
 join m n a v =
   gen (mulNat m n) a (\ (i : Nat) ->
-    at n a (at m (Vec n a) v (divNat i n)) (modNat i n));
+    at n a (at m (Vec a n) v (divNat i n)) (modNat i n));
 
 -- Split array into list
-split : (m n : Nat) -> (a : isort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
+split : (m n : Nat) -> (a : isort 0) -> Vec a (mulNat m n) -> Vec (Vec a n) m;
 split m n a v =
-  gen m (Vec n a) (\ (i : Nat) ->
+  gen m (Vec a n) (\ (i : Nat) ->
     gen n a (\ (j : Nat) ->
       at (mulNat m n) a v (addNat (mulNat i n) j)));
 
 -- Append two arrays together.
-append : (m n : Nat) -> (a : isort 0) -> Vec m a -> Vec n a -> Vec (addNat m n) a;
+append : (m n : Nat) -> (a : isort 0) -> Vec a m -> Vec a n -> Vec a (addNat m n);
 append m n a x y =
   gen (addNat m n) a
     (\ (i : Nat) ->
       ite a (ltNat i m) (at m a x i) (at n a y (subNat i m)));
 
 -- Rotate array to the left.
-primitive rotateL : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> Vec n a;
+primitive rotateL : (n : Nat) -> (a : sort 0) -> Vec a n -> Nat -> Vec a n;
 -- rotateL n a v i = gen n a (\ (j:Nat) -> at n a v (modNat (addNat i j) n));
 
 -- Rotate array to the right.
-primitive rotateR : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> Vec n a;
+primitive rotateR : (n : Nat) -> (a : sort 0) -> Vec a n -> Nat -> Vec a n;
 -- rotateR n a v i = gen n a (\ (j:Nat) -> at n a v (modNat (addNat (subNat n i) j) n));
 
 -- Shift array to the left.
-primitive shiftL : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> Vec n a;
+primitive shiftL : (n : Nat) -> (a : sort 0) -> a -> Vec a n -> Nat -> Vec a n;
 
 -- Shift array to the right.
-primitive shiftR : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> Vec n a;
+primitive shiftR : (n : Nat) -> (a : sort 0) -> a -> Vec a n -> Nat -> Vec a n;
 
 joinLittleEndian  : (m n : Nat)
                   -> (a : isort 0)
-                  -> Vec m (Vec n a)
-                  -> Vec (mulNat m n) a;
-joinLittleEndian m n a v = join m n a (reverse m (Vec n a) v);
+                  -> Vec (Vec a n) m
+                  -> Vec a (mulNat m n);
+joinLittleEndian m n a v = join m n a (reverse m (Vec a n) v);
 
 splitLittleEndian : (m n : Nat)
                   -> (a : isort 0)
-                  -> Vec (mulNat m n) a
-                  -> Vec m (Vec n a);
-splitLittleEndian m n a v = reverse m (Vec n a) (split m n a v);
+                  -> Vec a (mulNat m n)
+                  -> Vec (Vec a n) m;
+splitLittleEndian m n a v = reverse m (Vec a n) (split m n a v);
 
 -- Priority mux: Return the vector element corresponding to the first
 -- position where the select bit is true.
@@ -1727,7 +1727,7 @@ splitLittleEndian m n a v = reverse m (Vec n a) (split m n a v);
 -- Example:
 -- pmux 3 a [c0, c1, c2] [x0, x1, x2] y = ite a c0 x0 (ite a c1 x1 (ite a c2 x2 y))
 
-pmux : (n : Nat) -> (a : sort 0) -> Vec n Bool -> Vec n a -> a -> a;
+pmux : (n : Nat) -> (a : sort 0) -> Vec Bool n -> Vec a n -> a -> a;
 pmux n a conds xs default =
   foldr (a -> a) a n (id (a -> a)) default
   (zipWith Bool a (a -> a) (ite a) n conds xs);
@@ -1739,7 +1739,7 @@ primitive appendString : String -> String -> String;
 
 -- Convert a Cryptol string (a sequence of 8-bit ASCII characters) to a SAWCore
 -- String.
-primitive bytesToString : (n : Nat) -> Vec n (Vec 8 Bool) -> String;
+primitive bytesToString : (n : Nat) -> Vec (Vec Bool 8) n -> String;
 
 primitive equalString : String -> String -> Bool;
 
@@ -1749,87 +1749,87 @@ primitive equalString : String -> String -> Bool;
 -- Bitvector operations expect the most-significant bit first.
 
 -- | Returns most-significant bit in a signed bitvector.
-msb : (n : Nat) -> Vec (Succ n) Bool -> Bool;
+msb : (n : Nat) -> Vec Bool (Succ n) -> Bool;
 msb n v = at (Succ n) Bool v 0;
 
 -- | Returns least-significant bit in a bitvector.
-lsb : (n : Nat) -> Vec (Succ n) Bool -> Bool;
+lsb : (n : Nat) -> Vec Bool (Succ n) -> Bool;
 lsb n v = at (Succ n) Bool v n;
 
 -- | (bvNat n x) yields (x mod 2^n) as an n-bit vector.
-primitive bvNat : (n : Nat) -> Nat -> Vec n Bool;
+primitive bvNat : (n : Nat) -> Nat -> Vec Bool n;
 
 -- | Satisfies @bvNat n (bvToNat n x) = x@.
-primitive bvToNat : (n : Nat) -> Vec n Bool -> Nat;
+primitive bvToNat : (n : Nat) -> Vec Bool n -> Nat;
 
-axiom bvNat_bvToNat : (n : Nat) -> (x : Vec n Bool) ->
-                      Eq (Vec n Bool) (bvNat n (bvToNat n x)) x;
+axiom bvNat_bvToNat : (n : Nat) -> (x : Vec Bool n) ->
+                      Eq (Vec Bool n) (bvNat n (bvToNat n x)) x;
 
-bvAt : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool
+bvAt : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec a n -> Vec Bool w
      -> a;
 bvAt n a w xs i = at n a xs (bvToNat w i);
 
-bvUpd : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool
-      -> a -> Vec n a;
+bvUpd : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec a n -> Vec Bool w
+      -> a -> Vec a n;
 bvUpd n a w xs i y = upd n a xs (bvToNat w i) y;
 
-bvRotateL : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool -> Vec n a;
+bvRotateL : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec a n -> Vec Bool w -> Vec a n;
 bvRotateL n a w xs i = rotateL n a xs (bvToNat w i);
 
-bvRotateR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool -> Vec n a;
+bvRotateR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec a n -> Vec Bool w -> Vec a n;
 bvRotateR n a w xs i = rotateR n a xs (bvToNat w i);
 
-bvShiftL : (n : Nat) -> (a : isort 0) -> (w : Nat) -> a -> Vec n a -> Vec w Bool -> Vec n a;
+bvShiftL : (n : Nat) -> (a : isort 0) -> (w : Nat) -> a -> Vec a n -> Vec Bool w -> Vec a n;
 bvShiftL n a w z xs i = shiftL n a z xs (bvToNat w i);
 
-bvShiftR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> a -> Vec n a -> Vec w Bool -> Vec n a;
+bvShiftR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> a -> Vec a n -> Vec Bool w -> Vec a n;
 bvShiftR n a w z xs i = shiftR n a z xs (bvToNat w i);
 
 -- A version of bvShiftR that uses the 0th element of the input Vec as the default shift value
-bvSShiftR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec (Succ n) a -> Vec w Bool -> Vec (Succ n) a;
+bvSShiftR : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec a (Succ n) -> Vec Bool w -> Vec a (Succ n);
 bvSShiftR n a w xs i = bvShiftR (Succ n) a w (at (Succ n) a xs 0) xs i;
 
-primitive bvAdd : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+primitive bvAdd : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 
 -- | Unsigned and signed comparison functions.
-primitive bvugt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
-primitive bvuge : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
-primitive bvult : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
-primitive bvule : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+primitive bvugt : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
+primitive bvuge : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
+primitive bvult : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
+primitive bvule : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 
-primitive bvsgt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
-primitive bvsge : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
-primitive bvslt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
-primitive bvsle : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+primitive bvsgt : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
+primitive bvsge : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
+primitive bvslt : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
+primitive bvsle : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 
-primitive bvPopcount : (n : Nat) -> Vec n Bool -> Vec n Bool;
-primitive bvCountLeadingZeros : (n : Nat) -> Vec n Bool -> Vec n Bool;
-primitive bvCountTrailingZeros : (n : Nat) -> Vec n Bool -> Vec n Bool;
+primitive bvPopcount : (n : Nat) -> Vec Bool n -> Vec Bool n;
+primitive bvCountLeadingZeros : (n : Nat) -> Vec Bool n -> Vec Bool n;
+primitive bvCountTrailingZeros : (n : Nat) -> Vec Bool n -> Vec Bool n;
 
 -- Universal quantification over bitvectors
-primitive bvForall : (n : Nat) -> (Vec n Bool -> Bool) -> Bool;
+primitive bvForall : (n : Nat) -> (Vec Bool n -> Bool) -> Bool;
 
-bvCarry : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+bvCarry : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 bvCarry n x y = bvult n (bvAdd n x y) x;
 
-bvSCarry : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Bool;
+bvSCarry : (n : Nat) -> Vec Bool (Succ n) -> Vec Bool (Succ n) -> Bool;
 bvSCarry n x y = and (boolEq (msb n x) (msb n y)) (xor (msb n x) (msb n (bvAdd (Succ n) x y)));
 
-bvAddWithCarry : (n : Nat) -> Vec n Bool -> Vec n Bool -> #(Bool, Vec n Bool);
+bvAddWithCarry : (n : Nat) -> Vec Bool n -> Vec Bool n -> #(Bool, Vec Bool n);
 bvAddWithCarry n x y = (bvCarry n x y, bvAdd n x y);
 
-axiom bvAddZeroL : (n : Nat) -> (x : Vec n Bool) -> Eq (Vec n Bool) (bvAdd n (bvNat n 0) x) x;
-axiom bvAddZeroR : (n : Nat) -> (x : Vec n Bool) -> Eq (Vec n Bool) (bvAdd n x (bvNat n 0)) x;
+axiom bvAddZeroL : (n : Nat) -> (x : Vec Bool n) -> Eq (Vec Bool n) (bvAdd n (bvNat n 0) x) x;
+axiom bvAddZeroR : (n : Nat) -> (x : Vec Bool n) -> Eq (Vec Bool n) (bvAdd n x (bvNat n 0)) x;
 
-primitive bvNeg : (n : Nat) -> Vec n Bool -> Vec n Bool;
+primitive bvNeg : (n : Nat) -> Vec Bool n -> Vec Bool n;
 
-primitive bvSub : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+primitive bvSub : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 
-bvSBorrow : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Bool;
+bvSBorrow : (n : Nat) -> Vec Bool (Succ n) -> Vec Bool (Succ n) -> Bool;
 bvSBorrow n x y = and (xor (msb n x) (msb n y)) (xor (msb n x) (msb n (bvSub (Succ n) x y)));
 
-primitive bvMul : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
-primitive bvLg2 : (n : Nat) -> Vec n Bool -> Vec n Bool;
+primitive bvMul : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
+primitive bvLg2 : (n : Nat) -> Vec Bool n -> Vec Bool n;
 
 -- Unsigned division and remainder.
 --
@@ -1838,8 +1838,8 @@ primitive bvLg2 : (n : Nat) -> Vec n Bool -> Vec n Bool;
 --
 -- These two functions satisfy the property that:
 --   bvAdd x (bvMul x (bvUDiv x u v) v) (bvURem x u v) == u
-primitive bvUDiv : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
-primitive bvURem : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+primitive bvUDiv : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
+primitive bvURem : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 
 
 -- Signed division.
@@ -1854,134 +1854,134 @@ primitive bvURem : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
 -- bvSDiv and bvSRem satisfy the property that:
 --
 --   bvAdd x (bvMul x (bvSDiv x u v) v) (bvSRem x u v) == u
-primitive bvSDiv : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Vec (Succ n) Bool;
-primitive bvSRem : (n : Nat) -> Vec (Succ n) Bool -> Vec (Succ n) Bool -> Vec (Succ n) Bool;
+primitive bvSDiv : (n : Nat) -> Vec Bool (Succ n) -> Vec Bool (Succ n) -> Vec Bool (Succ n);
+primitive bvSRem : (n : Nat) -> Vec Bool (Succ n) -> Vec Bool (Succ n) -> Vec Bool (Succ n);
 --TODO:
 
 -- | Shift left by the given number of bits.
 -- New bits are False.
-primitive bvShl : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
+primitive bvShl : (w : Nat) -> Vec Bool w -> Nat -> Vec Bool w;
 
 -- Logical right shift.  New bits are False.
-primitive bvShr : (w : Nat) -> Vec w Bool -> Nat -> Vec w Bool;
+primitive bvShr : (w : Nat) -> Vec Bool w -> Nat -> Vec Bool w;
 
 -- | Signed right shift.  New bits are equal to most-significant bit.
-primitive bvSShr : (w : Nat) -> Vec (Succ w) Bool -> Nat -> Vec (Succ w) Bool;
+primitive bvSShr : (w : Nat) -> Vec Bool (Succ w) -> Nat -> Vec Bool (Succ w);
 
 axiom bvShiftL_bvShl :
-  (n : Nat) -> (w : Nat) -> (x : Vec n Bool) -> (i : Vec w Bool) ->
-  Eq (Vec n Bool) (bvShiftL n Bool w False x i) (bvShl n x (bvToNat w i));
+  (n : Nat) -> (w : Nat) -> (x : Vec Bool n) -> (i : Vec Bool w) ->
+  Eq (Vec Bool n) (bvShiftL n Bool w False x i) (bvShl n x (bvToNat w i));
 
 axiom bvShiftR_bvShr :
-  (n : Nat) -> (w : Nat) -> (x : Vec n Bool) -> (i : Vec w Bool) ->
-  Eq (Vec n Bool) (bvShiftR n Bool w False x i) (bvShr n x (bvToNat w i));
+  (n : Nat) -> (w : Nat) -> (x : Vec Bool n) -> (i : Vec Bool w) ->
+  Eq (Vec Bool n) (bvShiftR n Bool w False x i) (bvShr n x (bvToNat w i));
 
 -- | Zipwith specialized to bitvectors.
 bvZipWith : (Bool -> Bool -> Bool)
           -> (n : Nat)
-          -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+          -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 bvZipWith = zipWith Bool Bool Bool;
 
 -- | Bitwise complement.
-bvNot : (n : Nat) -> Vec n Bool -> Vec n Bool;
+bvNot : (n : Nat) -> Vec Bool n -> Vec Bool n;
 bvNot = map Bool Bool not;
 
 -- | Pairwise conjunction
-bvAnd : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+bvAnd : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 bvAnd = bvZipWith and;
 
 -- | Pairwise disjunction
-bvOr : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+bvOr : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 bvOr  = bvZipWith or;
 
 -- | Pairwise exclusive or
-bvXor : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+bvXor : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 bvXor = bvZipWith xor;
 
 -- | Return true if two bitvectors are equal.
-bvEq : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+bvEq : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 bvEq n x y = vecEq n Bool boolEq x y;
 
-axiom bvEq_refl : (n : Nat) -> (x : Vec n Bool) -> Eq Bool (bvEq n x x) True;
+axiom bvEq_refl : (n : Nat) -> (x : Vec Bool n) -> Eq Bool (bvEq n x x) True;
 
-axiom equalNat_bv : (n : Nat) -> (x : Vec n Bool) -> (i : Nat) ->
+axiom equalNat_bv : (n : Nat) -> (x : Vec Bool n) -> (i : Nat) ->
                Eq Bool (equalNat i (bvToNat n x)) (bvEq n (bvNat n i) x);
 
 -- | Returns the bitvector 1 if the boolean is true,
 --   and returns 0 otherwise
-bvBool : (n : Nat) -> Bool -> Vec n Bool;
-bvBool n b = ite (Vec n Bool) b (bvNat n 1) (bvNat n 0);
+bvBool : (n : Nat) -> Bool -> Vec Bool n;
+bvBool n b = ite (Vec Bool n) b (bvNat n 1) (bvNat n 0);
 
 -- | Return true if two bitvectors are not equal.
-bvNe : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+bvNe : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 bvNe n x y = not (bvEq n x y);
 
 -- | Return true if the bitvector is nonzero
-bvNonzero : (n : Nat) -> Vec n Bool -> Bool;
+bvNonzero : (n : Nat) -> Vec Bool n -> Bool;
 bvNonzero n x = bvNe n x (bvNat n 0);
 
 -- | Truncates a vector a smaller size.
 -- msb implementation:
-bvTrunc : (m n : Nat) -> Vec (addNat m n) Bool -> Vec n Bool;
+bvTrunc : (m n : Nat) -> Vec Bool (addNat m n) -> Vec Bool n;
 bvTrunc = drop Bool;
 -- lsb implementation:
--- bvTrunc : (m n : Nat) -> Vec (addNat n m) Bool -> Vec n Bool;
+-- bvTrunc : (m n : Nat) -> Vec Bool (addNat n m) -> Vec Bool n;
 -- bvTrunc m n = take Bool n m;
 
 -- | Perform a unsigned extension of the bitvector.
 -- @bvUExt m n x@ adds m bits of zeros to the most-significant bits of
 -- the n-bit vector x.
 -- msb implementation:
-bvUExt : (m n : Nat) -> Vec n Bool -> Vec (addNat m n) Bool;
+bvUExt : (m n : Nat) -> Vec Bool n -> Vec Bool (addNat m n);
 bvUExt m n x = append m n Bool (bvNat m 0) x;
 -- lsb implementation:
--- bvUExt : (m n : Nat) -> Vec n Bool -> Vec (addNat n m) Bool;
+-- bvUExt : (m n : Nat) -> Vec Bool n -> Vec Bool (addNat n m);
 -- bvUExt m n a = append n m Bool x (bvNat m 0);
 
 -- | 'replicateBool' is an version of 'replicate' optimized for type Bool.
-replicateBool : (n : Nat) -> Bool -> Vec n Bool;
-replicateBool n b = ite (Vec n Bool) b (bvNot n (bvNat n 0)) (bvNat n 0);
+replicateBool : (n : Nat) -> Bool -> Vec Bool n;
+replicateBool n b = ite (Vec Bool n) b (bvNot n (bvNat n 0)) (bvNat n 0);
 
 -- | Perform a signed extension of the bitvector.
 -- msb implementation:
-bvSExt : (m n : Nat) -> Vec (Succ n) Bool -> Vec (addNat m (Succ n)) Bool;
+bvSExt : (m n : Nat) -> Vec Bool (Succ n) -> Vec Bool (addNat m (Succ n));
 bvSExt m n x = append m (Succ n) Bool (replicateBool m (msb n x)) x;
 -- lsb implementation:
--- bvSExt : (m n : Nat) -> Vec (Succ n) Bool -> Vec (addNat (Succ n) m) Bool;
+-- bvSExt : (m n : Nat) -> Vec Bool (Succ n) -> Vec Bool (addNat (Succ n) m);
 -- bvSExt m n x = append (Succ n) m Bool x (replicateBool m (msb n x));
 
-bvMin : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
-bvMin n x y = ite (Vec n Bool) (bvule n x y) x y;
+bvMin : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
+bvMin n x y = ite (Vec Bool n) (bvule n x y) x y;
 
 --------------------------------------------------------------------------------
 -- GF2 Polynomials
 
 polyMul :
-  (m n : Nat) -> Vec (Succ m) Bool -> Vec (Succ n) Bool ->
-  Vec (Succ (addNat m n)) Bool;
+  (m n : Nat) -> Vec Bool (Succ m) -> Vec Bool (Succ n) ->
+  Vec Bool (Succ (addNat m n));
 polyMul m n x y =
-  foldl Bool (Vec (Succ (addNat m n)) Bool) (Succ n)
-  (\ (z : Vec (Succ (addNat m n)) Bool) (yi : Bool) ->
+  foldl Bool (Vec Bool (Succ (addNat m n))) (Succ n)
+  (\ (z : Vec Bool (Succ (addNat m n))) (yi : Bool) ->
    bvXor (Succ (addNat m n))
    (bvShl (Succ (addNat m n)) z 1)
-   (coerce (Vec (addNat n (Succ m)) Bool) (Vec (Succ (addNat m n)) Bool)
+   (coerce (Vec Bool (addNat n (Succ m))) (Vec Bool (Succ (addNat m n)))
     (vecCong Bool (addNat n (Succ m)) (Succ (addNat m n))
      (trans Nat (addNat n (Succ m)) (Succ (addNat n m)) (Succ (addNat m n))
       (eqNatAddS n m) (eqNatSucc (addNat n m) (addNat m n) (eqNatAddComm n m)))
     )
-    (bvUExt n (Succ m) ((ite (Vec (Succ m) Bool) yi x (bvNat (Succ m) 0))))
+    (bvUExt n (Succ m) ((ite (Vec Bool (Succ m)) yi x (bvNat (Succ m) 0))))
    )
   )
   (bvNat (Succ (addNat m n)) 0)
   y;
 
-polyMod : (m n : Nat) -> Vec m Bool -> Vec (Succ n) Bool -> Vec n Bool;
+polyMod : (m n : Nat) -> Vec Bool m -> Vec Bool (Succ n) -> Vec Bool n;
 polyMod m n x y =
-  (\ (reduce : Vec (Succ n) Bool -> Vec (Succ n) Bool) ->
-   (foldr Bool #(Vec n Bool, Vec (Succ n) Bool) m
-    (\ (xi : Bool) (acc : #(Vec n Bool, Vec (Succ n) Bool)) ->
+  (\ (reduce : Vec Bool (Succ n) -> Vec Bool (Succ n)) ->
+   (foldr Bool #(Vec Bool n, Vec Bool (Succ n)) m
+    (\ (xi : Bool) (acc : #(Vec Bool n, Vec Bool (Succ n))) ->
      (bvXor n (acc.0)
-      (ite (Vec n Bool) xi (tail n Bool (acc.1)) (bvNat n 0))
+      (ite (Vec Bool n) xi (tail n Bool (acc.1)) (bvNat n 0))
      ,
       reduce (bvShl (Succ n) (acc.1) 1)
      )
@@ -1989,7 +1989,7 @@ polyMod m n x y =
     (bvNat n 0, reduce (bvNat (Succ n) 1)) x
    ).0
   )
-  (\ (u : Vec (Succ n) Bool) -> bvMin (Succ n) u (bvXor (Succ n) u y));
+  (\ (u : Vec Bool (Succ n)) -> bvMin (Succ n) u (bvXor (Succ n) u y));
 
 --------------------------------------------------------------------------------
 -- Infinite streams
@@ -2012,7 +2012,7 @@ streamUpd a strm i y =
                  MkStream a (\ (j : Nat) -> ite a (equalNat i j) y (s j))) strm;
 
 bvStreamUpd : (a : sort 0) -> (w : Nat) ->
-     Stream a -> Vec w Bool -> a -> Stream a;
+     Stream a -> Vec Bool w -> a -> Stream a;
 bvStreamUpd a w xs i y = streamUpd a xs (bvToNat w i) y;
 
 streamGet : (a : sort 0) -> Stream a -> Nat -> a;
@@ -2030,28 +2030,28 @@ streamMap2 : (a b c : sort 0) -> (a -> b -> c) ->
 streamMap2 a b c f xs ys =
   MkStream c (\ (i : Nat) -> f (streamGet a xs i) (streamGet b ys i));
 
-streamTake : (a : sort 0) -> (n : Nat) -> Stream a -> Vec n a;
+streamTake : (a : sort 0) -> (n : Nat) -> Stream a -> Vec a n;
 streamTake a n xs = gen n a (\ (i : Nat) -> streamGet a xs i);
 
 streamDrop : (a : sort 0) -> (n : Nat) -> Stream a -> Stream a;
 streamDrop a n xs = MkStream a (\ (i : Nat) -> streamGet a xs (addNat n i));
 
-streamAppend : (a : sort 0) -> (n : Nat) -> Vec n a -> Stream a -> Stream a;
+streamAppend : (a : sort 0) -> (n : Nat) -> Vec a n -> Stream a -> Stream a;
 streamAppend a n xs ys =
   MkStream a (\ (i : Nat) ->
     atWithDefault n a (streamGet a ys (subNat i n)) xs i);
 
 streamJoin : (a : isort 0) -> (n : Nat)
-           -> Stream (Vec (Succ n) a)
+           -> Stream (Vec a (Succ n))
            -> (Stream a);
 streamJoin a n s =
   MkStream a (\ (i:Nat) ->
-     at (Succ n) a (streamGet (Vec (Succ n) a) s (divNat i (Succ n)))
+     at (Succ n) a (streamGet (Vec a (Succ n)) s (divNat i (Succ n)))
                    (modNat i (Succ n)) );
 
-streamSplit : (a : sort 0) -> (n : Nat) -> Stream a -> Stream (Vec n a);
+streamSplit : (a : sort 0) -> (n : Nat) -> Stream a -> Stream (Vec a n);
 streamSplit a n xs =
-  MkStream (Vec n a) (\ (i : Nat) ->
+  MkStream (Vec a n) (\ (i : Nat) ->
     gen n a (\ (j : Nat) ->
       streamGet a xs (addNat (mulNat i n) j)));
 
@@ -2108,13 +2108,13 @@ primitive natToInt : Nat -> Integer;
 
 -- for x >= 0, intToBv n x = x `mod` 2^n
 -- for x <  0, intToBv n x = bvNeg n (-x `mod` 2^n)
-primitive intToBv : (n:Nat) -> Integer -> Vec n Bool;
+primitive intToBv : (n:Nat) -> Integer -> Vec Bool n;
 
 -- return the unsigned value of the bitvector as an integer
-primitive bvToInt : (n:Nat) -> Vec n Bool -> Integer;
+primitive bvToInt : (n:Nat) -> Vec Bool n -> Integer;
 
 -- return the 2's complement signed value of the bitvector as an integer
-primitive sbvToInt : (n:Nat) -> Vec n Bool -> Integer;
+primitive sbvToInt : (n:Nat) -> Vec Bool n -> Integer;
 
 intEven : Integer -> Bool;
 intEven x = intEq (intMod x (natToInt 2)) (natToInt 0);
@@ -2143,7 +2143,7 @@ updNatFun : (a:sort 0)
 updNatFun a f i v x = ite a (equalNat i x) v (f x);
 
 updBvFun : (n:Nat) -> (a:sort 0)
-	 -> (Vec n Bool -> a) -> Vec n Bool -> a -> (Vec n Bool -> a);
+	 -> (Vec Bool n -> a) -> Vec Bool n -> a -> (Vec Bool n -> a);
 updBvFun n a f i v x = ite a (bvEq n i x) v (f x);
 
 --------------------------------------------------------------------------------
@@ -2154,15 +2154,15 @@ primitive Float : sort 0;
 
 -- mkFloat m e = m * 2^^e
 primitive mkFloat : Integer -> Integer -> Float;
--- primitive bvToFloat : Vec 32 Bool -> Float;
--- primitive floatToBV : Float -> Vec 32 Bool;
+-- primitive bvToFloat : Vec Bool 32 -> Float;
+-- primitive floatToBV : Float -> Vec Bool 32;
 
 primitive Double : sort 0;
 
 -- mkDouble m e = m * 2^^e
 primitive mkDouble : Integer -> Integer -> Float;
--- primitive bvToDouble : Vec 64 Bool -> Double;
--- primitive doubleToBV : Double -> Vec 64 Bool;
+-- primitive bvToDouble : Vec Bool 64 -> Double;
+-- primitive doubleToBV : Double -> Vec Bool 64;
 
 
 --------------------------------------------------------------------------------
@@ -2388,106 +2388,106 @@ arrowsSort as =
 -- Vector operations with built-in casts of their resulting lengths
 
 -- Specialized version of unsafeAssert for bitvector inequalities
-axiom unsafeAssertBVULt : (n : Nat) -> (x : Vec n Bool) -> (y : Vec n Bool) ->
+axiom unsafeAssertBVULt : (n : Nat) -> (x : Vec Bool n) -> (y : Vec Bool n) ->
                           Eq Bool (bvult n x y) True;
-axiom unsafeAssertBVULe : (n : Nat) -> (x : Vec n Bool) -> (y : Vec n Bool) ->
+axiom unsafeAssertBVULe : (n : Nat) -> (x : Vec Bool n) -> (y : Vec Bool n) ->
                           Eq Bool (bvule n x y) True;
 
 -- Convert a bvEq equality to an equality of bitvectors
-primitive bvEqToEq : (n : Nat) -> (v1 v2 : Vec n Bool) ->
-                     Eq Bool (bvEq n v1 v2) True -> Eq (Vec n Bool) v1 v2;
+primitive bvEqToEq : (n : Nat) -> (v1 v2 : Vec Bool n) ->
+                     Eq Bool (bvEq n v1 v2) True -> Eq (Vec Bool n) v1 v2;
 
 -- An ite on bitvector equality with a proof term in the True branch
-ifBvEqWithProof : (a : sort 0) -> (n : Nat) -> (v1 v2 : Vec n Bool) ->
-                  a -> (Eq (Vec n Bool) v1 v2 -> a) -> a;
+ifBvEqWithProof : (a : sort 0) -> (n : Nat) -> (v1 v2 : Vec Bool n) ->
+                  a -> (Eq (Vec Bool n) v1 v2 -> a) -> a;
 ifBvEqWithProof a n v1 v2 x f =
   ifWithProof a (bvEq n v1 v2) x
     (\ (pf:Eq Bool (bvEq n v1 v2) True) -> f (bvEqToEq n v1 v2 pf));
 
 -- Convert a proof of bitvector equality to one of Nat equality
-primitive bvEqToEqNat : (n : Nat) -> (v1 v2 : Vec n Bool) ->
-                        Eq (Vec n Bool) v1 v2 ->
+primitive bvEqToEqNat : (n : Nat) -> (v1 v2 : Vec Bool n) ->
+                        Eq (Vec Bool n) v1 v2 ->
                         eqNat (bvToNat n v1) (bvToNat n v2);
 
 -- Convert a proof of bitvector less-than to one of Nat less-than
-primitive bvultToIsLtNat : (n : Nat) -> (v1 v2 : Vec n Bool) ->
+primitive bvultToIsLtNat : (n : Nat) -> (v1 v2 : Vec Bool n) ->
                            Eq Bool (bvult n v1 v2) True ->
                            IsLtNat (bvToNat n v1) (bvToNat n v2);
 
 -- Generate a vector using a proof that the index is in the range of the vector
 -- FIXME: Like the below, gen should maybe use this...?
 primitive genWithProof : (n : Nat) -> (a : sort 0) ->
-                         ((i : Nat) -> IsLtNat i n -> a) -> Vec n a;
+                         ((i : Nat) -> IsLtNat i n -> a) -> Vec a n;
 
 -- | Index a vector using a proof that the index is in the range of the vector
 -- FIXME: atWithDefault should maybe use this...?
-primitive atWithProof : (n : Nat) -> (a : sort 0) -> Vec n a ->
+primitive atWithProof : (n : Nat) -> (a : sort 0) -> Vec a n ->
                         (i : Nat) -> IsLtNat i n -> a;
 
 -- Set the value at index i in a vector using a proof that i is in range
-primitive updWithProof : (n : Nat) -> (a : sort 0) -> Vec n a ->
-                         (i : Nat) -> a -> IsLtNat i n -> Vec n a;
+primitive updWithProof : (n : Nat) -> (a : sort 0) -> Vec a n ->
+                         (i : Nat) -> a -> IsLtNat i n -> Vec a n;
 
 -- Take a slice of a vector using a proof that the slice is in range
 primitive sliceWithProof : (a : sort 0) -> (n off len : Nat) ->
-                           IsLeNat (addNat off len) n -> Vec n a -> Vec len a;
+                           IsLeNat (addNat off len) n -> Vec a n -> Vec a len;
 
 -- Update a slice of a vector using a proof that the slice is in range
 primitive updSliceWithProof : (a : sort 0) -> (n off len : Nat) ->
                               IsLeNat (addNat off len) n ->
-                              Vec n a -> Vec len a -> Vec n a;
+                              Vec a n -> Vec a len -> Vec a n;
 
 
 --------------------------------------------------------------------------------
 -- Vectors indexed by bitvectors
 
 -- Helper definition to write the proposition that x <u y
-is_bvult : (n:Nat) -> (x y:Vec n Bool) -> Prop;
+is_bvult : (n:Nat) -> (x y:Vec Bool n) -> Prop;
 is_bvult n x y = Eq Bool (bvult n x y) True;
 
 -- Helper definition to write the proposition that x <=u y
-is_bvule : (n:Nat) -> (x y:Vec n Bool) -> Prop;
+is_bvule : (n:Nat) -> (x y:Vec Bool n) -> Prop;
 is_bvule n x y = Eq Bool (bvule n x y) True;
 
 -- Axiom: x <u 0 never hold
-axiom not_bvult_zero : (n:Nat) -> (x:Vec n Bool) ->
+axiom not_bvult_zero : (n:Nat) -> (x:Vec Bool n) ->
                        Eq Bool (bvult n x (bvNat n 0)) False;
 
 -- Axiom: x <=u y <u z implies x <u z
-axiom trans_bvult_bvule : (n:Nat) -> (x y z:Vec n Bool) ->
+axiom trans_bvult_bvule : (n:Nat) -> (x y z:Vec Bool n) ->
                           is_bvult n x y -> is_bvule n y z -> is_bvult n x z;
 
-axiom bvult_sub_add_bvult : (n:Nat) -> (x y z:Vec n Bool) ->
+axiom bvult_sub_add_bvult : (n:Nat) -> (x y z:Vec Bool n) ->
                             is_bvule n y z -> is_bvult n x (bvSub n z y) ->
                             is_bvult n (bvAdd n y x) z;
 
 -- Axiom: x <u y+z and y <=u x implies (x-y) <u z
-axiom bvult_sum_bvult_sub : (n:Nat) -> (x y z:Vec n Bool) ->
+axiom bvult_sum_bvult_sub : (n:Nat) -> (x y z:Vec Bool n) ->
                             is_bvult n x (bvAdd n y z) ->
                             Eq Bool (bvult n x y) False ->
                             is_bvult n (bvSub n x y) z;
 
 -- When comparing a nat and a bitvector, IsLtNat and is_bvult are equivalent
-axiom IsLtNat_to_bvult : (n : Nat) -> (x : Vec n Bool) -> (i : Nat) ->
+axiom IsLtNat_to_bvult : (n : Nat) -> (x : Vec Bool n) -> (i : Nat) ->
                          IsLtNat i (bvToNat n x) -> is_bvult n (bvNat n i) x;
-axiom bvult_to_IsLtNat : (n : Nat) -> (x : Vec n Bool) -> (i : Nat) ->
+axiom bvult_to_IsLtNat : (n : Nat) -> (x : Vec Bool n) -> (i : Nat) ->
                          is_bvult n (bvNat n i) x -> IsLtNat i (bvToNat n x);
 
 -- | The complete induction principle on bitvectors
 BV_complete_induction :
   (w: Nat) ->
-  (p: Vec w Bool -> Prop) ->
-  ((x : Vec w Bool) -> ((y: Vec w Bool) -> is_bvult w y x -> p y) -> p x) ->
-  (x : Vec w Bool) -> p x;
+  (p: Vec Bool w -> Prop) ->
+  ((x : Vec Bool w) -> ((y: Vec Bool w) -> is_bvult w y x -> p y) -> p x) ->
+  (x : Vec Bool w) -> p x;
 BV_complete_induction w p f x0 =
   Nat_complete_induction
-    (\ (n:Nat) -> (x:Vec w Bool) -> IsLeNat (bvToNat w x) n -> p x)
+    (\ (n:Nat) -> (x:Vec Bool w) -> IsLeNat (bvToNat w x) n -> p x)
     (\ (n:Nat) ->
-     \ (Hind : (m : Nat) -> (Hm : IsLtNat m n) -> (y : Vec w Bool) ->
+     \ (Hind : (m : Nat) -> (Hm : IsLtNat m n) -> (y : Vec Bool w) ->
                (Hy : IsLeNat (bvToNat w y) m) -> p y) ->
-     \ (x : Vec w Bool) ->
+     \ (x : Vec Bool w) ->
      \ (Hx : IsLeNat (bvToNat w x) n) ->
-       f x (\ (y:Vec w Bool) -> \ (Hult : is_bvult w y x) ->
+       f x (\ (y:Vec Bool w) -> \ (Hult : is_bvult w y x) ->
               Hind (bvToNat w y)
 	        (IsLeNat_transitive (Succ (bvToNat w y)) (bvToNat w x) n (bvultToIsLtNat w y x Hult) Hx)
 	        y (IsLeNat_base (bvToNat w y))
@@ -2504,9 +2504,9 @@ primitive Array : sort 0 -> sort 0 -> sort 0;
 primitive arrayConstant : (a b : sort 0) -> b -> (Array a b);
 primitive arrayLookup : (a b : sort 0) -> (Array a b) -> a -> b;
 primitive arrayUpdate : (a b : sort 0) -> (Array a b) -> a -> b -> (Array a b);
-primitive arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
-primitive arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
-primitive arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
+primitive arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec Bool n) a -> Vec Bool n -> Array (Vec Bool n) a -> Vec Bool n -> Vec Bool n -> Array (Vec Bool n) a;
+primitive arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec Bool n) a -> Vec Bool n -> a -> Vec Bool n -> Array (Vec Bool n) a;
+primitive arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec Bool n) a -> Vec Bool n -> Array (Vec Bool n) a -> Vec Bool n -> Vec Bool n -> Bool;
 primitive arrayEq     : (a b : sort 0) -> (Array a b) -> (Array a b) -> Bool;
 
 --------------------------------------------------------------------------------
@@ -2593,36 +2593,36 @@ rationalRoundToEven r =
 -- General axioms
 
 axiom bveq_sameL : (n : Nat)
-           -> (x z : Vec n Bool)
+           -> (x z : Vec Bool n)
            -> Eq Bool
                  (bvEq n x (bvAdd n x z))
                  (bvEq n (bvNat n 0) z);
 
 axiom bveq_sameR : (n : Nat)
-           -> (x y : Vec n Bool)
+           -> (x y : Vec Bool n)
            -> Eq Bool
                  (bvEq n (bvAdd n x y) x)
                  (bvEq n y (bvNat n 0));
 
 axiom bveq_same2 : (n : Nat)
-           -> (x y z : Vec n Bool)
+           -> (x y z : Vec Bool n)
            -> Eq Bool
                  (bvEq n (bvAdd n x y) (bvAdd n x z))
                  (bvEq n y z);
 
-axiom ite_split_cong : (b : Bool) -> (x : Vec 384 Bool) -> (y : Vec 384 Bool)
-               -> Eq (Vec 12 (Vec 32 Bool))
-                     (split 12 32 Bool (ite (Vec 384 Bool) b x y))
-                     (ite (Vec 12 (Vec 32 Bool)) b (split 12 32 Bool x) (split 12 32 Bool y));
+axiom ite_split_cong : (b : Bool) -> (x : Vec Bool 384) -> (y : Vec Bool 384)
+               -> Eq (Vec (Vec Bool 32) 12)
+                     (split 12 32 Bool (ite (Vec Bool 384) b x y))
+                     (ite (Vec (Vec Bool 32) 12) b (split 12 32 Bool x) (split 12 32 Bool y));
 
 axiom ite_join_cong : (b : Bool)
-              -> (x : Vec 12 (Vec 32 Bool))
-              -> (y : Vec 12 (Vec 32 Bool))
-              -> Eq (Vec 384 Bool)
-                    (join 12 32 Bool (ite (Vec 12 (Vec 32 Bool)) b x y))
-                    (ite (Vec 384 Bool) b (join 12 32 Bool x) (join 12 32 Bool y));
+              -> (x : Vec (Vec Bool 32) 12)
+              -> (y : Vec (Vec Bool 32) 12)
+              -> Eq (Vec Bool 384)
+                    (join 12 32 Bool (ite (Vec (Vec Bool 32) 12) b x y))
+                    (ite (Vec Bool 384) b (join 12 32 Bool x) (join 12 32 Bool y));
 
 axiom map_map : (a b c : sort 0) -> (f : a -> b) -> (g : b -> c) ->
-                 (n : Nat) -> (xs : Vec n a) ->
-                 Eq (Vec n c) (map b c g n (map a b f n xs))
+                 (n : Nat) -> (xs : Vec a n) ->
+                 Eq (Vec c n) (map b c g n (map a b f n xs))
                               (map a c (\ (x:a) -> g (f x)) n xs);
diff --git a/saw-core/src/SAWCore/FiniteValue.hs b/saw-core/src/SAWCore/FiniteValue.hs
index 8860a02cf6..f3d69429f7 100644
--- a/saw-core/src/SAWCore/FiniteValue.hs
+++ b/saw-core/src/SAWCore/FiniteValue.hs
@@ -357,7 +357,7 @@ asFiniteType sc t = do
   case t' of
     (R.asBoolType -> Just ())
       -> return FTBit
-    (R.isVecType return -> Just (n R.:*: tp))
+    (R.isVecType return -> Just (tp R.:*: n))
       -> FTVec n <$> asFiniteType sc tp
     (R.asTupleType -> Just ts)
       -> FTTuple <$> traverse (asFiniteType sc) ts
@@ -387,7 +387,7 @@ asFirstOrderTypeMaybe sc t =
          -> return (FOTIntMod n)
        (R.asRationalType -> Just ())
          -> return FOTRational
-       (R.isVecType return -> Just (n R.:*: tp))
+       (R.isVecType return -> Just (tp R.:*: n))
          -> FOTVec n <$> asFirstOrderTypeMaybe sc tp
        (R.asArrayType -> Just (tp1 R.:*: tp2)) -> do
          tp1' <- asFirstOrderTypeMaybe sc tp1
@@ -404,7 +404,7 @@ asFiniteTypePure :: Term -> Maybe FiniteType
 asFiniteTypePure t =
   case t of
     (R.asBoolType -> Just ()) -> Just FTBit
-    (R.isVecType return -> Just (n R.:*: tp)) -> FTVec n <$> asFiniteTypePure tp
+    (R.isVecType return -> Just (tp R.:*: n)) -> FTVec n <$> asFiniteTypePure tp
     (R.asTupleType -> Just ts) -> FTTuple <$> traverse asFiniteTypePure ts
     (R.asRecordType -> Just fs) -> FTRec <$> traverse asFiniteTypePure (Map.fromList fs)
     _ -> Nothing
@@ -428,7 +428,7 @@ scFirstOrderType sc ft =
     FOTRational -> scRationalType sc
     FOTVec n t  -> do n' <- scNat sc n
                       t' <- scFirstOrderType sc t
-                      scVecType sc n' t'
+                      scVecType sc t' n'
     FOTArray t1 t2 -> do t1' <- scFirstOrderType sc t1
                          t2' <- scFirstOrderType sc t2
                          scArrayType sc t1' t2'
diff --git a/saw-core/src/SAWCore/OpenTerm.hs b/saw-core/src/SAWCore/OpenTerm.hs
index 03d845e251..d6e17c1243 100644
--- a/saw-core/src/SAWCore/OpenTerm.hs
+++ b/saw-core/src/SAWCore/OpenTerm.hs
@@ -161,13 +161,13 @@ bvLit bits =
 
 -- | Create a SAW core term for a vector type
 vectorType :: OpenTerm -> OpenTerm -> OpenTerm
-vectorType n a = applyGlobal "Prelude.Vec" [n,a]
+vectorType a n = applyGlobal "Prelude.Vec" [a, n]
 
 -- | Create a SAW core term for the type of a bitvector
 bvType :: Integral a => a -> OpenTerm
 bvType n =
   apply (global "Prelude.Vec")
-  [nat (fromIntegral n), boolType]
+  [boolType, nat (fromIntegral n)]
 
 -- | Build an 'OpenTerm' for a pair
 pair :: OpenTerm -> OpenTerm -> OpenTerm
@@ -336,7 +336,7 @@ sawLet x tp tp_ret rhs body_f =
 -- | Build a bitvector type with the given length
 bitvectorType :: OpenTerm -> OpenTerm
 bitvectorType w =
-  applyGlobal "Prelude.Vec" [w, global "Prelude.Bool"]
+  applyGlobal "Prelude.Vec" [global "Prelude.Bool", w]
 
 -- | Build a SAW core term for a list with the given element type
 list :: OpenTerm -> [OpenTerm] -> OpenTerm
diff --git a/saw-core/src/SAWCore/Recognizer.hs b/saw-core/src/SAWCore/Recognizer.hs
index c1fb98c5e0..007e8bc110 100644
--- a/saw-core/src/SAWCore/Recognizer.hs
+++ b/saw-core/src/SAWCore/Recognizer.hs
@@ -443,14 +443,14 @@ asRationalType = isGlobalDef "Prelude.Rational"
 asVectorType :: Recognizer Term (Term, Term)
 asVectorType = fmap toPair . ((isGlobalDef "Prelude.Vec" @> return) <@> return)
 
-isVecType :: Recognizer Term a -> Recognizer Term (Natural :*: a)
-isVecType tp = (isGlobalDef "Prelude.Vec" @> asNat) <@> tp
+isVecType :: Recognizer Term a -> Recognizer Term (a :*: Natural)
+isVecType tp = (isGlobalDef "Prelude.Vec" @> tp) <@> asNat
 
-asVecType :: Recognizer Term (Natural :*: Term)
+asVecType :: Recognizer Term (Term :*: Natural)
 asVecType = isVecType return
 
 asBitvectorType :: Recognizer Term Natural
-asBitvectorType = (isGlobalDef "Prelude.Vec" @> asNat) <@ asBoolType
+asBitvectorType = (isGlobalDef "Prelude.Vec" @> asBoolType) @> asNat
 
 asMux :: Recognizer Term (Term :*: Term :*: Term :*: Term)
 asMux = isGlobalDef "Prelude.ite" @> return <@> return <@> return <@> return
diff --git a/saw-core/src/SAWCore/SharedTerm.hs b/saw-core/src/SAWCore/SharedTerm.hs
index a684fb2704..b87579eabf 100644
--- a/saw-core/src/SAWCore/SharedTerm.hs
+++ b/saw-core/src/SAWCore/SharedTerm.hs
@@ -1387,10 +1387,10 @@ scNatType sc = scGlobalDef sc preludeNatIdent
 -- | Create a term representing a vector type, from a term giving the length
 -- and a term giving the element type.
 scVecType :: SharedContext
-          -> Term -- ^ The length of the vector
           -> Term -- ^ The element type
+          -> Term -- ^ The length of the vector
           -> IO Term
-scVecType sc n e = scGlobalApply sc preludeVecIdent [n, e]
+scVecType sc e n = scGlobalApply sc preludeVecIdent [e, n]
 
 -- | Create a term applying @Prelude.not@ to the given term.
 --
@@ -1431,7 +1431,7 @@ scBoolEq sc x y = scGlobalApply sc "Prelude.boolEq" [x,y]
 
 -- | Create a universally quantified bitvector term.
 --
--- > bvForall : (n : Nat) -> (Vec n Bool -> Bool) -> Bool;
+-- > bvForall : (n : Nat) -> (Vec Bool n -> Bool) -> Bool;
 scBvForall :: SharedContext -> Term -> Term -> IO Term
 scBvForall sc w f = scGlobalApply sc "Prelude.bvForall" [w, f]
 
@@ -1463,33 +1463,33 @@ scOrList sc = disj . filter nontrivial
 
 -- | Create a term applying @Prelude.append@ to two vectors.
 --
--- > append : (m n : Nat) -> (e : sort 0) -> Vec m e -> Vec n e -> Vec (addNat m n) e;
+-- > append : (m n : Nat) -> (e : sort 0) -> Vec e m -> Vec e n -> Vec e (addNat m n);
 scAppend :: SharedContext -> Term -> Term -> Term ->
             Term -> Term -> IO Term
 scAppend sc m n t x y = scGlobalApply sc "Prelude.append" [m, n, t, x, y]
 
 -- | Create a term applying @Prelude.join@ to a vector of vectors.
 --
--- > join  : (m n : Nat) -> (a : sort 0) -> Vec m (Vec n a) -> Vec (mulNat m n) a;
+-- > join  : (m n : Nat) -> (a : sort 0) -> Vec (Vec a n) m -> Vec a (mulNat m n);
 scJoin :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
 scJoin sc m n a v = scGlobalApply sc "Prelude.join" [m, n, a, v]
 
 -- | Create a term splitting a vector with @Prelude.split@.
 --
--- > split : (m n : Nat) -> (a : sort 0) -> Vec (mulNat m n) a -> Vec m (Vec n a);
+-- > split : (m n : Nat) -> (a : sort 0) -> Vec a (mulNat m n) -> Vec (Vec a n) m;
 scSplit :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
 scSplit sc m n a v = scGlobalApply sc "Prelude.split" [m, n, a, v]
 
 -- | Create a term selecting a range of values from a vector with @Prelude.slice@.
 --
--- > slice : (e : sort 1) -> (i n o : Nat) -> Vec (addNat (addNat i n) o) e -> Vec n e;
+-- > slice : (e : sort 1) -> (i n o : Nat) -> Vec e (addNat (addNat i n) o) -> Vec e n;
 scSlice :: SharedContext -> Term -> Term ->
            Term -> Term -> Term -> IO Term
 scSlice sc e i n o a = scGlobalApply sc "Prelude.slice" [e, i, n, o, a]
 
 -- | Create a term accessing a particular element of a vector with @get@.
 --
--- > get : (n : Nat) -> (e : sort 0) -> Vec n e -> Fin n -> e;
+-- > get : (n : Nat) -> (e : sort 0) -> Vec e n -> Fin n -> e;
 scGet :: SharedContext -> Term -> Term ->
          Term -> Term -> IO Term
 scGet sc n e v i = scGlobalApply sc (mkIdent preludeName "get") [n, e, v, i]
@@ -1497,7 +1497,7 @@ scGet sc n e v i = scGlobalApply sc (mkIdent preludeName "get") [n, e, v, i]
 -- | Create a term accessing a particular element of a vector with @bvAt@,
 -- which uses a bitvector for indexing.
 --
--- > bvAt : (n : Nat) -> (a : sort 0) -> (w : Nat) -> Vec n a -> Vec w Bool -> a;
+-- > bvAt : (n : Nat) -> (a : sort 0) -> (w : Nat) -> Vec a n -> Vec Bool w -> a;
 scBvAt :: SharedContext -> Term -> Term ->
          Term -> Term -> Term -> IO Term
 scBvAt sc n a i xs idx = scGlobalApply sc (mkIdent preludeName "bvAt") [n, a, i, xs, idx]
@@ -1505,35 +1505,35 @@ scBvAt sc n a i xs idx = scGlobalApply sc (mkIdent preludeName "bvAt") [n, a, i,
 -- | Create a term accessing a particular element of a vector, with a default
 -- to return if the index is out of bounds.
 --
--- > atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec n a -> Nat -> a;
+-- > atWithDefault : (n : Nat) -> (a : sort 0) -> a -> Vec a n -> Nat -> a;
 scAtWithDefault :: SharedContext -> Term -> Term -> Term -> Term -> Term -> IO Term
 scAtWithDefault sc n a v xs idx = scGlobalApply sc (mkIdent preludeName "atWithDefault") [n, a, v, xs, idx]
 
 -- | Create a term accessing a particular element of a vector, failing if the
 -- index is out of bounds.
 --
--- > at : (n : Nat) -> (a : sort 0) -> Vec n a -> Nat -> a;
+-- > at : (n : Nat) -> (a : sort 0) -> Vec a n -> Nat -> a;
 scAt :: SharedContext -> Term -> Term ->
         Term -> Term -> IO Term
 scAt sc n a xs idx = scGlobalApply sc (mkIdent preludeName "at") [n, a, xs, idx]
 
 -- | Create a term evaluating to a vector containing a single element.
 --
--- > single : (e : sort 1) -> e -> Vec 1 e;
+-- > single : (e : sort 1) -> e -> Vec e 1;
 scSingle :: SharedContext -> Term -> Term -> IO Term
 scSingle sc e x = scGlobalApply sc (mkIdent preludeName "single") [e, x]
 
 -- | Create a term computing the least significant bit of a bitvector, given a
 -- length and bitvector.
 --
--- > lsb : (n : Nat) -> Vec (Succ n) Bool -> Bool;
+-- > lsb : (n : Nat) -> Vec Bool (Succ n) -> Bool;
 scLsb :: SharedContext -> Term -> Term -> IO Term
 scLsb sc n x = scGlobalApply sc (mkIdent preludeName "lsb") [n, x]
 
 -- | Create a term computing the most significant bit of a bitvector, given a
 -- length and bitvector.
 --
--- > msb : (n : Nat) -> Vec (Succ n) Bool -> Bool;
+-- > msb : (n : Nat) -> Vec Bool (Succ n) -> Bool;
 scMsb :: SharedContext -> Term -> Term -> IO Term
 scMsb sc n x = scGlobalApply sc (mkIdent preludeName "lsb") [n, x]
 
@@ -1709,7 +1709,7 @@ scNatToInt sc x = scGlobalApply sc "Prelude.natToInt" [x]
 -- | Create a term computing a bitvector of length n from an @Integer@, if
 -- possible.
 --
--- > intToBv : (n::Nat) -> Integer -> Vec n Bool;
+-- > intToBv : (n::Nat) -> Integer -> Vec Bool n;
 scIntToBv
    :: SharedContext -> Term -> Term -> IO Term
 scIntToBv sc n x = scGlobalApply sc "Prelude.intToBv" [n,x]
@@ -1717,7 +1717,7 @@ scIntToBv sc n x = scGlobalApply sc "Prelude.intToBv" [n,x]
 -- | Create a term computing an @Integer@ from a bitvector of length n.
 -- This produces the unsigned value of the bitvector.
 --
--- > bvToInt : (n : Nat) -> Vec n Bool -> Integer;
+-- > bvToInt : (n : Nat) -> Vec Bool n -> Integer;
 scBvToInt
    :: SharedContext -> Term -> Term -> IO Term
 scBvToInt sc n x = scGlobalApply sc "Prelude.bvToInt" [n,x]
@@ -1725,7 +1725,7 @@ scBvToInt sc n x = scGlobalApply sc "Prelude.bvToInt" [n,x]
 -- | Create a term computing an @Integer@ from a bitvector of length n.
 -- This produces the 2's complement signed value of the bitvector.
 --
--- > sbvToInt : (n : Nat) -> Vec n Bool -> Integer;
+-- > sbvToInt : (n : Nat) -> Vec Bool n -> Integer;
 scSbvToInt
    :: SharedContext -> Term -> Term -> IO Term
 scSbvToInt sc n x = scGlobalApply sc "Prelude.sbvToInt" [n,x]
@@ -1791,17 +1791,17 @@ scBitvector :: SharedContext -> Natural -> IO Term
 scBitvector sc size =
   do s <- scNat sc size
      t <- scBoolType sc
-     scVecType sc s t
+     scVecType sc t s
 
 -- | Create a term computing a bitvector of length x from a @Nat@, if possible.
 --
--- > bvNat : (n : Nat) -> Nat -> Vec n Bool;
+-- > bvNat : (n : Nat) -> Nat -> Vec Bool n;
 scBvNat :: SharedContext -> Term -> Term -> IO Term
 scBvNat sc x y = scGlobalApply sc "Prelude.bvNat" [x, y]
 
 -- | Create a term computing a @Nat@ from a bitvector of length n.
 --
--- > bvToNat : (n : Nat) -> Vec n Bool -> Nat;
+-- > bvToNat : (n : Nat) -> Vec Bool n -> Nat;
 scBvToNat :: SharedContext -> Natural -> Term -> IO Term
 scBvToNat sc n x = do
     n' <- scNat sc n
@@ -1828,206 +1828,206 @@ scBvLit sc w v = assert (w <= fromIntegral (maxBound :: Int)) $ do
 -- the other given term evaluates to @False@ and representing 1 if the other
 -- given term evaluates to @True@.
 --
--- > bvBool : (n : Nat) -> Bool -> Vec n Bool;
+-- > bvBool : (n : Nat) -> Bool -> Vec Bool n;
 scBvBool :: SharedContext -> Term -> Term -> IO Term
 scBvBool sc n x = scGlobalApply sc "Prelude.bvBool" [n, x]
 
 -- | Create a term returning true if and only if the given bitvector represents
 -- a nonzero value.
 --
--- > bvNonzero : (n : Nat) -> Vec n Bool -> Bool;
+-- > bvNonzero : (n : Nat) -> Vec Bool n -> Bool;
 scBvNonzero :: SharedContext -> Term -> Term -> IO Term
 scBvNonzero sc n x = scGlobalApply sc "Prelude.bvNonzero" [n, x]
 
 -- | Create a term computing the 2's complement negation of the given
 -- bitvector.
--- > bvNeg : (n : Nat) -> Vec n Bool -> Vec n Bool;
+-- > bvNeg : (n : Nat) -> Vec Bool n -> Vec Bool n;
 scBvNeg :: SharedContext -> Term -> Term -> IO Term
 scBvNeg sc n x = scGlobalApply sc "Prelude.bvNeg" [n, x]
 
 -- | Create a term applying the bitvector addition primitive.
 --
--- > bvAdd : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvAdd : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvAdd :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvAdd sc n x y = scGlobalApply sc "Prelude.bvAdd" [n, x, y]
 
 -- | Create a term applying the bitvector subtraction primitive.
 --
--- > bvSub : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvSub : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvSub :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSub sc n x y = scGlobalApply sc "Prelude.bvSub" [n, x, y]
 
 -- | Create a term applying the bitvector multiplication primitive.
 --
--- > bvMul : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvMul : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvMul :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvMul sc n x y = scGlobalApply sc "Prelude.bvMul" [n, x, y]
 
 -- | Create a term applying the bitvector (unsigned) modulus primitive.
 --
--- > bvURem : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvURem : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvURem :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvURem sc n x y = scGlobalApply sc "Prelude.bvURem" [n, x, y]
 
 -- | Create a term applying the bitvector (unsigned) division primitive.
 --
--- > bvUDiv : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvUDiv : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvUDiv :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvUDiv sc n x y = scGlobalApply sc "Prelude.bvUDiv" [n, x, y]
 
 -- | Create a term applying the bitvector (signed) modulus primitive.
 --
--- > bvSRem : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvSRem : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvSRem :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSRem sc n x y = scGlobalApply sc "Prelude.bvSRem" [n, x, y]
 
 -- | Create a term applying the bitvector (signed) division primitive.
 --
--- > bvSDiv : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvSDiv : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvSDiv :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSDiv sc n x y = scGlobalApply sc "Prelude.bvSDiv" [n, x, y]
 
 -- | Create a term applying the lg2 bitvector primitive.
 --
--- > bvLg2 : (n : Nat) -> Vec n Bool -> Vec n Bool;
+-- > bvLg2 : (n : Nat) -> Vec Bool n -> Vec Bool n;
 scBvLg2 :: SharedContext -> Term -> Term -> IO Term
 scBvLg2 sc n x = scGlobalApply sc "Prelude.bvLg2" [n, x]
 
 -- | Create a term applying the population count bitvector primitive.
 --
--- > bvPopcount : (n : Nat) -> Vec n Bool -> Vec n Bool;
+-- > bvPopcount : (n : Nat) -> Vec Bool n -> Vec Bool n;
 scBvPopcount :: SharedContext -> Term -> Term -> IO Term
 scBvPopcount sc n x = scGlobalApply sc "Prelude.bvPopcount" [n, x]
 
 -- | Create a term applying the leading zero counting bitvector primitive.
 --
--- > bvCountLeadingZeros : (n : Nat) -> Vec n Bool -> Vec n Bool;
+-- > bvCountLeadingZeros : (n : Nat) -> Vec Bool n -> Vec Bool n;
 scBvCountLeadingZeros :: SharedContext -> Term -> Term -> IO Term
 scBvCountLeadingZeros sc n x = scGlobalApply sc "Prelude.bvCountLeadingZeros" [n, x]
 
 -- | Create a term applying the trailing zero counting bitvector primitive.
 --
--- > bvCountTrailingZeros : (n : Nat) -> Vec n Bool -> Vec n Bool;
+-- > bvCountTrailingZeros : (n : Nat) -> Vec Bool n -> Vec Bool n;
 scBvCountTrailingZeros :: SharedContext -> Term -> Term -> IO Term
 scBvCountTrailingZeros sc n x = scGlobalApply sc "Prelude.bvCountTrailingZeros" [n, x]
 
 -- | Create a term applying the bit-wise and primitive.
 --
--- > bvAnd : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvAnd : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvAnd :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvAnd sc n x y = scGlobalApply sc "Prelude.bvAnd" [n, x, y]
 
 -- | Create a term applying the bit-wise xor primitive.
 --
--- > bvXor : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvXor : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvXor :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvXor sc n x y = scGlobalApply sc "Prelude.bvXor" [n, x, y]
 
 -- | Create a term applying the bit-wise or primitive.
 --
--- > bvOr : (n : Nat) -> Vec n Bool -> Vec n Bool -> Vec n Bool;
+-- > bvOr : (n : Nat) -> Vec Bool n -> Vec Bool n -> Vec Bool n;
 scBvOr :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvOr  sc n x y = scGlobalApply sc "Prelude.bvOr"  [n, x, y]
 
 -- | Create a term applying the bit-wise negation primitive.
 --
--- > bvNot : (n : Nat) -> Vec n Bool -> Vec n Bool;
+-- > bvNot : (n : Nat) -> Vec Bool n -> Vec Bool n;
 scBvNot :: SharedContext -> Term -> Term -> IO Term
 scBvNot sc n x = scGlobalApply sc "Prelude.bvNot" [n, x]
 
 -- | Create a term computing whether the two given bitvectors (of equal length)
 -- are equal.
 --
--- > bvEq : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvEq : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvEq :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvEq  sc n x y = scGlobalApply sc "Prelude.bvEq"  [n, x, y]
 
 -- | Create a term applying the bitvector (unsigned) greater-than-or-equal
 -- primitive.
 --
--- > bvuge : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvuge : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvUGe :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvUGe sc n x y = scGlobalApply sc "Prelude.bvuge" [n, x, y]
 
 -- | Create a term applying the bitvector (unsigned) less-than-or-equal
 -- primitive.
 --
--- > bvule : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvule : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvULe :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvULe sc n x y = scGlobalApply sc "Prelude.bvule" [n, x, y]
 
 -- | Create a term applying the bitvector (unsigned) greater-than primitive.
 --
--- > bvugt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvugt : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvUGt :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvUGt sc n x y = scGlobalApply sc "Prelude.bvugt" [n, x, y]
 
 -- | Create a term applying the bitvector (unsigned) less-than primitive.
 --
--- > bvult : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvult : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvULt :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvULt sc n x y = scGlobalApply sc "Prelude.bvult" [n, x, y]
 
 -- | Create a term applying the bitvector (signed) greater-than-or-equal
 -- primitive.
 --
--- > bvsge : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvsge : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvSGe :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSGe sc n x y = scGlobalApply sc "Prelude.bvsge" [n, x, y]
 
 -- | Create a term applying the bitvector (signed) less-than-or-equal
 -- primitive.
 --
--- > bvsle : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvsle : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvSLe :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSLe sc n x y = scGlobalApply sc "Prelude.bvsle" [n, x, y]
 
 -- | Create a term applying the bitvector (signed) greater-than primitive.
 --
--- > bvsgt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvsgt : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvSGt :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSGt sc n x y = scGlobalApply sc "Prelude.bvsgt" [n, x, y]
 
 -- | Create a term applying the bitvector (signed) less-than primitive.
 --
--- > bvslt : (n : Nat) -> Vec n Bool -> Vec n Bool -> Bool;
+-- > bvslt : (n : Nat) -> Vec Bool n -> Vec Bool n -> Bool;
 scBvSLt :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSLt sc n x y = scGlobalApply sc "Prelude.bvslt" [n, x, y]
 
 -- | Create a term applying the left-shift primitive.
 --
--- > bvShl : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool;
+-- > bvShl : (n : Nat) -> Vec Bool n -> Nat -> Vec Bool n;
 scBvShl :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvShl sc n x y = scGlobalApply sc "Prelude.bvShl" [n, x, y]
 
 -- | Create a term applying the logical right-shift primitive.
 --
--- > bvShr : (n : Nat) -> Vec n Bool -> Nat -> Vec n Bool;
+-- > bvShr : (n : Nat) -> Vec Bool n -> Nat -> Vec Bool n;
 scBvShr :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvShr sc n x y = scGlobalApply sc "Prelude.bvShr" [n, x, y]
 
 -- | Create a term applying the arithmetic/signed right-shift primitive.
 --
--- > bvSShr : (w : Nat) -> Vec (Succ w) Bool -> Nat -> Vec (Succ w) Bool;
+-- > bvSShr : (w : Nat) -> Vec Bool (Succ w) -> Nat -> Vec Bool (Succ w);
 scBvSShr :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSShr sc n x y = scGlobalApply sc "Prelude.bvSShr" [n, x, y]
 
 -- | Create a term applying the unsigned bitvector extension primitive.
 --
--- > bvUExt : (m n : Nat) -> Vec n Bool -> Vec (addNat m n) Bool;
+-- > bvUExt : (m n : Nat) -> Vec Bool n -> Vec Bool (addNat m n);
 scBvUExt :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvUExt sc n m x = scGlobalApply sc "Prelude.bvUExt" [n,m,x]
 
 -- | Create a term applying the signed bitvector extension primitive.
 --
--- > bvSExt : (m n : Nat) -> Vec (Succ n) Bool -> Vec (addNat m (Succ n)) Bool;
+-- > bvSExt : (m n : Nat) -> Vec Bool (Succ n) -> Vec Bool (addNat m (Succ n));
 scBvSExt :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvSExt sc n m x = scGlobalApply sc "Prelude.bvSExt" [n,m,x]
 
 -- | Create a term applying the bitvector truncation primitive. Note that this
 -- truncates starting from the most significant bit.
 --
--- > bvTrunc : (m n : Nat) -> Vec (addNat m n) Bool -> Vec n Bool;
+-- > bvTrunc : (m n : Nat) -> Vec Bool (addNat m n) -> Vec Bool n;
 scBvTrunc :: SharedContext -> Term -> Term -> Term -> IO Term
 scBvTrunc sc n m x = scGlobalApply sc "Prelude.bvTrunc" [n,m,x]
 
@@ -2044,7 +2044,7 @@ scUpdNatFun sc a f i v = scGlobalApply sc "Prelude.updNatFun" [a, f, i, v]
 -- | Create a term applying the @updBvFun@ primitive, which has the same
 -- behavior as @updNatFun@ but acts on bitvectors.
 --
--- > updBvFun : (n : Nat) -> (a : sort 0) -> (Vec n Bool -> a) -> Vec n Bool -> a -> (Vec n Bool -> a);
+-- > updBvFun : (n : Nat) -> (a : sort 0) -> (Vec Bool n -> a) -> Vec Bool n -> a -> (Vec Bool n -> a);
 scUpdBvFun :: SharedContext -> Term -> Term
            -> Term -> Term -> Term -> IO Term
 scUpdBvFun sc n a f i v = scGlobalApply sc "Prelude.updBvFun" [n, a, f, i, v]
@@ -2081,17 +2081,17 @@ scArrayUpdate sc a b f i e = scGlobalApply sc "Prelude.arrayUpdate" [a, b, f, i,
 scArrayEq :: SharedContext -> Term -> Term -> Term -> Term -> IO Term
 scArrayEq sc a b x y = scGlobalApply sc "Prelude.arrayEq" [a, b, x, y]
 
--- > arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Array (Vec n Bool) a;
+-- > arrayCopy : (n : Nat) -> (a : sort 0) -> Array (Vec Bool n) a -> Vec Bool n -> Array (Vec Bool n) a -> Vec Bool n -> Vec Bool n -> Array (Vec Bool n) a;
 -- > arrayCopy n a dest_arr dest_idx src_arr src_idx len
 scArrayCopy :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
 scArrayCopy sc n a f i g j l = scGlobalApply sc "Prelude.arrayCopy" [n, a, f, i, g, j, l]
 
--- > arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> a -> Vec n Bool -> Array (Vec n Bool) a;
+-- > arraySet : (n : Nat) -> (a : sort 0) -> Array (Vec Bool n) a -> Vec Bool n -> a -> Vec Bool n -> Array (Vec Bool n) a;
 -- > arraySet n a arr idx val len
 scArraySet :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
 scArraySet sc n a f i e l = scGlobalApply sc "Prelude.arraySet" [n, a, f, i, e, l]
 
--- > arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec n Bool) a -> Vec n Bool -> Array (Vec n Bool) a -> Vec n Bool -> Vec n Bool -> Bool;
+-- > arrayRangeEq : (n : Nat) -> (a : sort 0) -> Array (Vec Bool n) a -> Vec Bool n -> Array (Vec Bool n) a -> Vec Bool n -> Vec Bool n -> Bool;
 -- > arrayRangeEq n a lhs_arr lhs_idx rhs_arr rhs_idx len
 scArrayRangeEq :: SharedContext -> Term -> Term -> Term -> Term -> Term -> Term -> Term -> IO Term
 scArrayRangeEq sc n a f i g j l = scGlobalApply sc "Prelude.arrayRangeEq" [n, a, f, i, g, j, l]
diff --git a/saw-core/src/SAWCore/Simulator/Prims.hs b/saw-core/src/SAWCore/Simulator/Prims.hs
index 54fce4d082..641e3be55b 100644
--- a/saw-core/src/SAWCore/Simulator/Prims.hs
+++ b/saw-core/src/SAWCore/Simulator/Prims.hs
@@ -850,11 +850,11 @@ equalStringOp bp =
 
 --------------------------------------------------------------------------------
 
--- Vec :: (n :: Nat) -> (a :: sort 0) -> sort 0;
+-- Vec :: (a :: sort 0) -> (n :: Nat) -> sort 0;
 vecTypeOp :: VMonad l => Prim l
 vecTypeOp =
-  natFun $ \n ->
   tvalFun $ \a ->
+  natFun $ \n ->
     PrimValue (TValue (VVecType n a))
 
 -- gen :: (n :: Nat) -> (a :: sort 0) -> (Nat -> a) -> Vec n a;
diff --git a/saw-core/src/SAWCore/Term/Certified.hs b/saw-core/src/SAWCore/Term/Certified.hs
index 16c24aa402..839f9f3b6b 100644
--- a/saw-core/src/SAWCore/Term/Certified.hs
+++ b/saw-core/src/SAWCore/Term/Certified.hs
@@ -1855,13 +1855,13 @@ scmVector e xs =
      mapM_ check xs
      n <- scmNat (fromIntegral (length xs))
      let tf = FTermF (ArrayValue e (V.fromList xs))
-     ty <- scmVecType n e
+     ty <- scmVecType e n
      scmMakeTerm vt tf (Right ty)
 
--- | Create a term representing a vector type, from a term giving the length
--- and a term giving the element type.
+-- | Create a term representing a vector type, from a term giving the
+-- element type and a term giving the length.
 scmVecType :: Term -> Term -> SCM Term
-scmVecType n e = scmGlobalApply preludeVecIdent [n, e]
+scmVecType e n = scmGlobalApply preludeVecIdent [e, n]
 
 -- | Create a record term from a list of record fields.
 scmRecordValue :: [(FieldName, Term)] -> SCM Term