diff --git a/CHANGES.md b/CHANGES.md
new file mode 100644
--- /dev/null
+++ b/CHANGES.md
@@ -0,0 +1,9 @@
+Changelog for lol project
+================================
+
+0.1.0.0
+-----
+ * Fixed bug in Box-Muller sampling routine.
+ * Changed how we lift linear functions for better noise control.
+ * Split entailment functions in Tensor.
+ * Increased performance in FastCyc by better handling Sub constructors.
diff --git a/README b/README
--- a/README
+++ b/README
@@ -24,11 +24,11 @@
 * CTensor.hs, which gives an
   implementation of the Tensor class using a C backend via Haskell's FFI.
 
-* FiniteField.hs, which gives an unoptimized implementation of finite field
-  arithmetic. To use this module, you will need an instance of IrreduciblePoly.
-  These instances provide irreducible polynomials for various degrees and base fields.
-  One instance is provided for characteristic 2 fields of size up to 2^32 in 
-  IrreducibleChar2.hs.
+* FiniteField.hs, which gives an unoptimized implementation of finite
+  field arithmetic. To use this module, you will need an instance of
+  IrreduciblePoly.  These instances provide irreducible polynomials
+  for various degrees and base fields.  One instance is provided for
+  characteristic 2 fields of size up to 2^32 in IrreducibleChar2.hs.
 
 * ZqBasic.hs, which is a basic implementation of Zq=Z/qZ arithmetic.
 
diff --git a/lol.cabal b/lol.cabal
--- a/lol.cabal
+++ b/lol.cabal
@@ -5,19 +5,19 @@
 -- PVP summary:      +-+------- breaking API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             0.0.1.0
-synopsis:            A general-purpose library for lattice cryptography.
+version:             0.1.0.0
+synopsis:            A library for lattice cryptography.
 homepage:            https://github.com/cpeikert/Lol
 Bug-Reports:         https://github.com/cpeikert/Lol/issues
 license:             GPL-2
 license-file:        LICENSE
-author:              Eric Crockett, Chris Peikert
+author:              Eric Crockett <ecrockett0@gmail.com>, Chris Peikert <cpeikert@alum.mit.edu>
 maintainer:          Eric Crockett <ecrockett0@gmail.com>
 copyright:           Eric Crockett, Chris Peikert
 category:            Crypto
 stability:           experimental
 build-type:          Simple
-extra-source-files:  README, 
+extra-source-files:  README, CHANGES.md,
                      src/Crypto/Lol/Cyclotomic/Tensor/CTensor/tensorTypes.h,
                      test-suite/CycTests.hs,
                      test-suite/SHETests.hs,
@@ -25,7 +25,7 @@
                      test-suite/TestTypes.hs,
                      test-suite/ZqTests.hs
 cabal-version:       >=1.10
-description:         \\Lambda \\ocirc \\lambda is a general-purpose library for ring-based lattice cryptography.
+description:         Λ ○ λ (Lol) is a general-purpose library for ring-based lattice cryptography.
 source-repository head
   type: git
   location: https://github.com/cpeikert/Lol
diff --git a/src/Crypto/Lol/Applications/SymmSHE.hs b/src/Crypto/Lol/Applications/SymmSHE.hs
--- a/src/Crypto/Lol/Applications/SymmSHE.hs
+++ b/src/Crypto/Lol/Applications/SymmSHE.hs
@@ -25,7 +25,7 @@
 , embedSK, embedCT, twaceCT
 , tunnelCT
 -- * Constraint synonyms
-, AddPublicCtx, MulPublicCtx, KeySwitchCtx, KSHintCtx, ModSwitchPTCtx
+, AddPublicCtx, MulPublicCtx, InnerKeySwitchCtx, KeySwitchCtx, KSHintCtx, ModSwitchPTCtx
 , ToSDCtx, EncryptCtx, TunnelCtx, GenSKCtx, DecryptCtx
 , ErrorTermCtx
 ) where
@@ -97,14 +97,14 @@
    m `Divides` m')
 
 -- | Encrypt a plaintext under a secret key.
-encrypt :: forall t m m' z zp zq e rnd . (EncryptCtx t m m' z zp zq, MonadRandom rnd)
+encrypt :: forall t m m' z zp zq rnd . (EncryptCtx t m m' z zp zq, MonadRandom rnd)
            => SK (Cyc t m' z) -> PT (Cyc t m zp) -> rnd (CT m zp (Cyc t m' zq))
 encrypt (SK svar s) =
-  let sq = reduce s
-  in (\pt -> do
-         e <- errorCoset svar (embed pt :: PT (Cyc t m' zp))
-         c1 <- getRandom
-         return $! CT LSD zero one $ fromCoeffs [reduce e - c1 * sq, c1])
+  let sq = adviseCRT $ reduce s
+  in \pt -> do
+    e <- errorCoset svar (embed pt :: PT (Cyc t m' zp))
+    c1 <- getRandom
+    return $! CT LSD zero one $ fromCoeffs [reduce e - c1 * sq, c1]
 
 -- | Constraint synonym for extracting the error term of a ciphertext.
 type ErrorTermCtx t m' z zp zq =
@@ -228,10 +228,11 @@
 lweSample :: (LWECtx t m' z zq, MonadRandom rnd)
              => SK (Cyc t m' z) -> rnd (Polynomial (Cyc t m' zq))
 lweSample (SK svar s) =
-  let sq = adviseCRT $ negate $ reduce s
+  -- adviseCRT because we call `replicateM (lweSample s)` below, but only want to do CRT once. 
+  let sq = adviseCRT $ negate $ reduce s 
   in do
     e <- errorRounded svar
-    c1 <- getRandom
+    c1 <- adviseCRT <$> getRandom -- we would like hints to be in CRT form
     return $ fromCoeffs [c1 * sq + reduce (e `asTypeOf` s), c1]
 
 -- | Constraint synonym for generating key-switch hints.
@@ -245,7 +246,7 @@
 ksHint :: (KSHintCtx gad t m' z zq, MonadRandom rnd)
           => SK (Cyc t m' z) -> Cyc t m' z
           -> rnd (Tagged gad [Polynomial (Cyc t m' zq)])
-ksHint skout val = do           -- rnd monad
+ksHint skout val = do -- rnd monad
   let valq = reduce val
       valgad = encode valq
   -- CJP: clunky, but that's what we get without a MonadTagged
@@ -261,6 +262,7 @@
 
 knapsack :: forall t m' z zq' . (KnapsackCtx t m' z zq')
             => [Polynomial (Cyc t m' zq')] -> [Cyc t m' z] -> Polynomial (Cyc t m' zq')
+-- adviseCRT here because we are about to map (*) onto each polynomial coeff
 knapsack hint xs = sum (zipWith (*>>) (adviseCRT <$> reduce <$> xs) hint)
 
 type InnerKeySwitchCtx gad t m' zq zq' =
@@ -276,10 +278,7 @@
 
 -- | Constraint synonym for key switching.
 type KeySwitchCtx gad t m' zp zq zq' =
-  (ToSDCtx t m' zp zq,
-   -- EAC: same as InnerKeySwitchCtx, but duplicated for haddock
-   RescaleCyc (Cyc t) zq' zq, RescaleCyc (Cyc t) zq zq',
-   Decompose gad zq', KnapsackCtx t m' (DecompOf zq') zq')
+  (ToSDCtx t m' zp zq, InnerKeySwitchCtx gad t m' zq zq')
 
 -- | Switch a linear ciphertext under @s_in@ to a linear one under @s_out@
 keySwitchLinear :: forall gad t m' zp zq zq' z rnd m .
@@ -451,9 +450,11 @@
 twaceCT (CT d 0 l c) = CT d 0 l (twace <$> c)
 twaceCT _ = error "twaceCT requires 0 factors of g; call absorbGFactors first"
 
+
 -- | Constraint synonym for ring tunneling.
 type TunnelCtx t e r s e' r' s' z zp zq zq' gad =
   (ExtendLinIdx e r s e' r' s',     -- liftLin
+   e' ~ (e * (r' / r)),             -- convenience; implied by prev constraint
    KSHintCtx gad t r' z zq',        -- ksHint
    Reduce z zq,                     -- Reduce on Linear
    Lift zp z,                       -- liftLin
@@ -473,6 +474,7 @@
 tunnelCT f skout (SK _ sin) = tagT $ (do -- in rnd
   -- generate hints
   let f' = extendLin $ lift f :: Linear t z e' r' s'
+      f'q = reduce f' :: Linear t zq e' r' s'
       -- choice of basis here must match coeffsCyc basis below
       ps = proxy powBasis (Proxy::Proxy e')
       comps = (evalLin f' . (adviseCRT sin *)) <$> ps
@@ -481,7 +483,7 @@
     let CT MSD 0 s c = toMSD $ absorbGFactors ct'
         [c0,c1] = coeffs c
         -- apply E-linear function to constant term c0
-        c0' = evalLin (reduce f' :: Linear t zq e' r' s') c0
+        c0' = evalLin f'q c0
         -- apply E-linear function to c1 via key-switching
         -- this basis must match the basis used above to generate the hints
         c1s = coeffsCyc Pow c1 :: [Cyc t e' zq]
diff --git a/src/Crypto/Lol/Cyclotomic/Cyc.hs b/src/Crypto/Lol/Cyclotomic/Cyc.hs
--- a/src/Crypto/Lol/Cyclotomic/Cyc.hs
+++ b/src/Crypto/Lol/Cyclotomic/Cyc.hs
@@ -18,7 +18,7 @@
 -- * Basic operations
 , mulG, divG
 , scalarCyc, liftCyc
-, adviseCRT
+, advisePow, adviseDec, adviseCRT
 -- * Error sampling
 , tGaussian, errorRounded, errorCoset
 -- * Sub/extension rings
@@ -48,10 +48,11 @@
 newtype Cyc t m r = Cyc { 
   -- | Unsafe deconstructor for 'Cyc'.
   unsafeUnCyc :: UCyc t m r }
-                    deriving (Arbitrary, NFData, Random)
+                    deriving (Arbitrary, Random)
 
 -- See: https://ghc.haskell.org/trac/ghc/ticket/11008
 -- for why I have to use StandaloneDeriving here
+deriving instance NFData (UCyc t m a) => NFData (Cyc t m a)
 deriving instance Show (UCyc t m a) => Show (Cyc t m a)
 deriving instance Eq (UCyc t m a) => Eq (Cyc t m a)
 deriving instance Additive (UCyc t m a) => Additive.C (Cyc t m a)
@@ -94,12 +95,20 @@
 
 ---------- Core cyclotomic operations ----------
 
+adviseCRT, advisePow, adviseDec :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r
+
 -- | Yield an equivalent element that /may/ be in a CRT
 -- representation.  This can serve as an optimization hint. E.g.,
 -- call 'adviseCRT' prior to multiplying the same value by many
 -- other values.
-adviseCRT :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r
 adviseCRT = coerceCyc U.adviseCRT
+
+-- | Same as 'adviseCRT', but for the powerful-basis representation.
+advisePow = coerceCyc U.forcePow -- do it, but not required by contract
+
+-- | Same as 'adviseCRT', but for the powerful-basis representation.
+adviseDec = coerceCyc U.forceDec
+
 
 -- | Multiply by the special element @g@ of the @m@th cyclotomic.
 mulG :: (Fact m, CElt t r) => Cyc t m r -> Cyc t m r
diff --git a/src/Crypto/Lol/Cyclotomic/Linear.hs b/src/Crypto/Lol/Cyclotomic/Linear.hs
--- a/src/Crypto/Lol/Cyclotomic/Linear.hs
+++ b/src/Crypto/Lol/Cyclotomic/Linear.hs
@@ -1,8 +1,8 @@
 {-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts,
              GeneralizedNewtypeDeriving, KindSignatures,
              MultiParamTypeClasses, NoImplicitPrelude, RoleAnnotations,
-             ScopedTypeVariables, TypeFamilies, TypeOperators,
-             UndecidableInstances #-}
+             ScopedTypeVariables, StandaloneDeriving,
+             TypeFamilies, TypeOperators, UndecidableInstances #-}
 
 -- | Functions from one cyclotomic ring to another that are linear
 -- over a common subring.
@@ -22,8 +22,9 @@
 
 -- | An @E@-linear function from @R@ to @S@.
 newtype Linear t z (e::Factored) (r::Factored) (s::Factored) = D [Cyc t s z]
-  deriving (NFData)
 
+deriving instance (NFData (Cyc t s z)) => NFData (Linear t z e r s)
+
 -- TODO: have constructor for both relative Pow basis of R/E?
 
 -- some params are phantom but matter for safety
@@ -35,17 +36,17 @@
 linearDec :: forall t z e r s .
              (e `Divides` r, e `Divides` s, CElt t z)
              => [Cyc t s z] -> Linear t z e r s
-linearDec cs = let ps = proxy powBasis (Proxy::Proxy e) `asTypeOf` cs
-               in if length cs <= length ps then D (adviseCRT <$> cs)
+linearDec ys = let ps = proxy powBasis (Proxy::Proxy e) `asTypeOf` ys
+               in if length ys <= length ps then D (adviseCRT <$> ys)
                else error $ "linearDec: too many entries: "
-                           ++ show (length cs) ++ " versus "
+                           ++ show (length ys) ++ " versus "
                            ++ show (length ps)
 
 -- | Evaluates the given linear function on the input.
 evalLin :: forall t z e r s .
            (e `Divides` r, e `Divides` s, CElt t z)
            => Linear t z e r s -> Cyc t r z -> Cyc t s z
-evalLin (D cs) r = sum (zipWith (*) cs $
+evalLin (D ys) r = sum (zipWith (*) ys $
                         embed <$> (coeffsCyc Dec r :: [Cyc t e z]))
 
 instance Additive (Cyc t s z) => Additive.C (Linear t z e r s) where
@@ -60,21 +61,19 @@
 
 instance (Reduce z zq, Fact s, CElt t z, CElt t zq)
          => Reduce (Linear t z e r s) (Linear t zq e r s) where
-  reduce (D cs) = D $ reduce <$> cs
+  reduce (D ys) = D $ reduce <$> ys
 
 instance (CElt t zp, CElt t z, z ~ LiftOf zp, Lift zp z, Fact s)
          => Lift' (Linear t zp e r s) where
   type LiftOf (Linear t zp e r s) = Linear t (LiftOf zp) e r s
 
-  lift (D cs) = D $ liftCyc Dec <$> cs
+  lift (D ys) = D $ liftCyc Pow <$> ys
 
 -- | A convenient constraint synonym for extending a linear function
 -- to larger rings.
 type ExtendLinIdx e r s e' r' s' =
-  (e ~ FGCD r e', r' ~ FLCM r e', -- these imply R'=R\otimes_E E'
-   e' ~ (e * (r' / r)), -- just to help GHC. This is implied by previous two constraints
-   e' `Divides` s', s `Divides` s', -- these imply lcm(s,e')|s' <==> (S+E') \subseteq S'
-   Fact r) -- need Fact r because nothing else gives it
+  (Fact r, e ~ FGCD r e', r' ~ FLCM r e', -- these imply R'=R\otimes_E E'
+   e' `Divides` s', s `Divides` s') -- lcm(s,e')|s' <=> (S+E') \subseteq S'
 
 -- | Extend an @E@-linear function @R->S@ to an @E'@-linear function
 -- @R\'->S\'@.  (Mathematically, such extension only requires
@@ -87,4 +86,4 @@
 -- identical decoding bases, because R' \cong R \otimes_E E'.  If we
 -- relax the constraint on E then we'd have to change the
 -- implementation to something more difficult.
-extendLin (D cs) = D (embed <$> cs)
+extendLin (D ys) = D (embed <$> ys)
diff --git a/src/Crypto/Lol/Cyclotomic/Tensor.hs b/src/Crypto/Lol/Cyclotomic/Tensor.hs
--- a/src/Crypto/Lol/Cyclotomic/Tensor.hs
+++ b/src/Crypto/Lol/Cyclotomic/Tensor.hs
@@ -51,6 +51,7 @@
 class (TElt t Double, TElt t (Complex Double))
       => Tensor (t :: Factored -> * -> *) where
 
+  -- | Constraints needed by @t@ to hold type @r@.
   type TElt t r :: Constraint
 
   -- | Properties that hold for any index. Use with '\\'.
@@ -59,32 +60,39 @@
   
   -- | Properties that hold for any (legal) fully-applied tensor. Use
   -- with '\\'.
-  entailFullT :: Tagged (t m r)
-                 ((Fact m, TElt t r) :- 
-                  (Eq (t m r), ZeroTestable (t m r), Ring (t m r), 
-                   NFData (t m r), Random (t m r)))
+  entailEqT :: Tagged (t m r)
+               ((Eq r, Fact m, TElt t r) :- (Eq (t m r)))
+  entailZTT :: Tagged (t m r)
+               ((ZeroTestable r, Fact m, TElt t r) :- (ZeroTestable (t m r)))
+  entailRingT :: Tagged (t m r)
+                 ((Ring r, Fact m, TElt t r) :- (Ring (t m r)))
+  entailNFDataT :: Tagged (t m r)
+                   ((NFData r, Fact m, TElt t r) :- (NFData (t m r)))
+  entailRandomT :: Tagged (t m r)
+                   ((Random r, Fact m, TElt t r) :- (Random (t m r)))
 
   -- | Converts a scalar to a tensor in the powerful basis
-  scalarPow :: (Fact m, TElt t r) => r -> t m r
+  scalarPow :: (Ring r, Fact m, TElt t r) => r -> t m r
 
   -- | 'l' converts from decoding-basis representation to
   -- powerful-basis representation; 'lInv' is its inverse.
-  l, lInv :: (Fact m, TElt t r) => t m r -> t m r
+  l, lInv :: (Ring r, Fact m, TElt t r) => t m r -> t m r
 
   -- | Multiply by @g@ in the powerful/decoding basis
-  mulGPow, mulGDec :: (Fact m, TElt t r) => t m r -> t m r
+  mulGPow, mulGDec :: (Ring r, Fact m, TElt t r) => t m r -> t m r
 
   -- | Divide by @g@ in the powerful/decoding basis.  The 'Maybe'
   -- output indicates that the operation may fail, which happens
   -- exactly when the input is not divisible by @g@.
-  divGPow, divGDec :: (Fact m, TElt t r) => t m r -> Maybe (t m r)
+  divGPow, divGDec :: (ZeroTestable r, IntegralDomain r, Fact m, TElt t r)
+                      => t m r -> Maybe (t m r)
 
   -- | A tuple of all the operations relating to the CRT basis, in a
   -- single 'Maybe' value for safety.  Clients should typically not
   -- use this method directly, but instead call the corresponding
   -- top-level functions: the elements of the tuple correpond to the
   -- functions 'scalarCRT', 'mulGCRT', 'divGCRT', 'crt', 'crtInv'.
-  crtFuncs :: (Fact m, TElt t r, CRTrans r) =>
+  crtFuncs :: (ZeroTestable r, IntegralDomain r, CRTrans r, Fact m, TElt t r) =>
               Maybe (    r -> t m r, -- scalarCRT
                      t m r -> t m r, -- mulGCRT
                      t m r -> t m r, -- divGCRT
@@ -93,17 +101,17 @@
 
   -- | Sample from the "skewed" Gaussian error distribution @t*D@
   -- in the decoding basis, where @D@ has scaled variance @v@.
-  tGaussianDec :: (Fact m, OrdFloat q, Random q, TElt t q,
-                   ToRational v, MonadRandom rnd)
+  tGaussianDec :: (OrdFloat q, Random q, TElt t q,
+                   ToRational v, Fact m, MonadRandom rnd)
                   => v -> rnd (t m q)
 
   -- | The @twace@ linear transformation, which is the same in both the
   -- powerful and decoding bases.
-  twacePowDec :: (m `Divides` m', TElt t r) => t m' r -> t m r
+  twacePowDec :: (Ring r, m `Divides` m', TElt t r) => t m' r -> t m r
 
   -- | The @embed@ linear transformations, for the powerful and
   -- decoding bases.
-  embedPow, embedDec :: (m `Divides` m', TElt t r)
+  embedPow, embedDec :: (Ring r, m `Divides` m', TElt t r)
                         => t m r -> t m' r
 
   -- | A tuple of all the extension-related operations involving the
@@ -111,21 +119,22 @@
   -- method directly, but instead call the corresponding top-level
   -- functions: the elements of the tuple correpond to the functions
   -- 'twaceCRT', 'embedCRT'.
-  crtExtFuncs :: (m `Divides` m', TElt t r, CRTrans r) =>
+  crtExtFuncs :: (ZeroTestable r, IntegralDomain r, CRTrans r,
+                  m `Divides` m', TElt t r) =>
                  Maybe (t m' r -> t m  r, -- twaceCRT
                         t m  r -> t m' r) -- embedCRT
 
   -- | Map a tensor in the powerful\/decoding\/CRT basis, representing
   -- an @O_m'@ element, to a vector of tensors representing @O_m@
   -- elements in the same kind of basis.
-  coeffs :: (m `Divides` m', TElt t r) => t m' r -> [t m r]
+  coeffs :: (Ring r, m `Divides` m', TElt t r) => t m' r -> [t m r]
 
   -- | The powerful extension basis w.r.t. the powerful basis.
-  powBasisPow :: (m `Divides` m', TElt t r) => Tagged m [t m' r]
+  powBasisPow :: (Ring r, TElt t r, m `Divides` m') => Tagged m [t m' r]
 
   -- | A list of tensors representing the mod-@p@ CRT set of the
   -- extension.
-  crtSetDec :: (m `Divides` m', PrimeField fp,
+  crtSetDec :: (PrimeField fp, m `Divides` m',
                 Coprime (PToF (CharOf fp)) m', TElt t fp)
                => Tagged m [t m' fp]
 
@@ -137,7 +146,8 @@
              => (a -> mon b) -> t m a -> mon (t m b)
 
 -- | Convenience value indicating whether 'crtFuncs' exists.
-hasCRTFuncs :: forall t m r . (Tensor t, Fact m, TElt t r, CRTrans r)
+hasCRTFuncs :: forall t m r . (ZeroTestable r, IntegralDomain r, CRTrans r, 
+                               Tensor t, Fact m, TElt t r)
                => TaggedT (t m r) Maybe ()
 hasCRTFuncs = tagT $ do
   (_ :: r -> t m r,_,_,_,_) <- crtFuncs
@@ -145,11 +155,13 @@
 
 -- | Yield a tensor for a scalar in the CRT basis.  (This function is
 -- simply an appropriate entry from 'crtFuncs'.)
-scalarCRT :: (Tensor t, Fact m, TElt t r, CRTrans r) => Maybe (r -> t m r)
+scalarCRT :: (ZeroTestable r, IntegralDomain r, CRTrans r, 
+              Tensor t, Fact m, TElt t r) => Maybe (r -> t m r)
 scalarCRT = (\(f,_,_,_,_) -> f) <$> crtFuncs
 
 
-mulGCRT, divGCRT, crt, crtInv :: (Tensor t, Fact m, TElt t r, CRTrans r)
+mulGCRT, divGCRT, crt, crtInv ::
+  (ZeroTestable r, IntegralDomain r, CRTrans r, Tensor t, Fact m, TElt t r)
   => Maybe (t m r -> t m r)
 -- | Multiply by @g@ in the CRT basis. (This function is simply an
 -- appropriate entry from 'crtFuncs'.)
@@ -168,17 +180,18 @@
 -- For cyclotomic indices m | m',
 -- @Tw(x) = (mhat\/m\'hat) * Tr(g\'\/g * x)@.
 -- (This function is simply an appropriate entry from 'crtExtFuncs'.)
-twaceCRT :: forall t r m m' . (Tensor t, m `Divides` m', TElt t r, CRTrans r)
+twaceCRT :: forall t r m m' . (ZeroTestable r, IntegralDomain r, CRTrans r, 
+                               Tensor t, m `Divides` m', TElt t r)
             => Maybe (t m' r -> t m r)
 twaceCRT = proxyT hasCRTFuncs (Proxy::Proxy (t m' r)) *>
            proxyT hasCRTFuncs (Proxy::Proxy (t m  r)) *>
            (fst <$> crtExtFuncs)
 
-
 -- | Embed a tensor with index @m@ in the CRT basis to a tensor with
 -- index @m'@ in the CRT basis.
 -- (This function is simply an appropriate entry from 'crtExtFuncs'.)
-embedCRT :: forall t r m m' . (Tensor t, m `Divides` m', TElt t r, CRTrans r)
+embedCRT :: forall t r m m' . (ZeroTestable r, IntegralDomain r, CRTrans r, 
+                               Tensor t, m `Divides` m', TElt t r)
             => Maybe (t m r -> t m' r)
 embedCRT = proxyT hasCRTFuncs (Proxy::Proxy (t m' r)) *>
            proxyT hasCRTFuncs (Proxy::Proxy (t m  r)) *>
diff --git a/src/Crypto/Lol/Cyclotomic/Tensor/CTensor.hs b/src/Crypto/Lol/Cyclotomic/Tensor/CTensor.hs
--- a/src/Crypto/Lol/Cyclotomic/Tensor/CTensor.hs
+++ b/src/Crypto/Lol/Cyclotomic/Tensor/CTensor.hs
@@ -164,13 +164,16 @@
 
 instance Tensor CT where
 
-  type TElt CT r = (IntegralDomain r, ZeroTestable r, 
-                    Eq r, Random r, NFData r,
-                    Storable r, CRNS r)
+  type TElt CT r = (Storable r, CRNS r)
 
   entailIndexT = tag $ Sub Dict
-  entailFullT = tag $ Sub Dict
+  entailEqT = tag $ Sub Dict
+  entailZTT = tag $ Sub Dict
+  entailRingT = tag $ Sub Dict
+  entailNFDataT = tag $ Sub Dict
+  entailRandomT = tag $ Sub Dict
 
+
   scalarPow = CT . scalarPow' -- Vector code
 
   l = wrap $ lgWrapper $ untag $ lgDispatch dl
@@ -234,24 +237,24 @@
 -- | Class to dispatch to the C backend for various element types.
 class CRNS r where
 
-  zipWrapper :: (Fact m) => 
-    (forall a . (TElt CT a, Dispatch a) => CT' m a -> CT' m a -> CT' m a)
+  zipWrapper :: (Fact m, Additive r) => 
+    (forall a . (TElt CT a, Dispatch a, Additive a) => CT' m a -> CT' m a -> CT' m a)
     -> CT' m r -> CT' m r -> CT' m r
 
-  crtWrapper :: (Fact m, CRTrans r) => 
-    (forall a . (TElt CT a, CRTrans a, Dispatch a) => Maybe (CT' m a -> CT' m a))
+  crtWrapper :: (Fact m, CRTrans r, ZeroTestable r, IntegralDomain r) => 
+    (forall a . (TElt CT a, CRTrans a, Dispatch a, ZeroTestable a, IntegralDomain a) => Maybe (CT' m a -> CT' m a))
     -> Maybe (CT' m r -> CT' m r)
 
-  lgWrapper :: (Fact m) => 
-    (forall a . (TElt CT a, Dispatch a) => CT' m a -> CT' m a)
+  lgWrapper :: (Fact m, Additive r) => 
+    (forall a . (TElt CT a, Dispatch a, Additive a) => CT' m a -> CT' m a)
     -> CT' m r -> CT' m r
 
-  divGWrapper :: (Fact m) => 
-    (forall a . (TElt CT a, Dispatch a) => CT' m a -> Maybe (CT' m a))
+  divGWrapper :: (Fact m, IntegralDomain r, ZeroTestable r) => 
+    (forall a . (TElt CT a, Dispatch a, IntegralDomain a, ZeroTestable a) => CT' m a -> Maybe (CT' m a))
     -> CT' m r -> Maybe (CT' m r)
 
-  gaussWrapper :: (Fact m, MonadRandom rnd) => 
-    (forall a . (TElt CT a, Dispatch a, OrdFloat a, MonadRandom rnd) => rnd (CT' m a))
+  gaussWrapper :: (Fact m, MonadRandom rnd, Random r) => 
+    (forall a . (TElt CT a, Dispatch a, OrdFloat a, MonadRandom rnd, Random a) => rnd (CT' m a))
     -> rnd (CT' m r)
 
 instance CRNS Double where
@@ -283,7 +286,12 @@
   divGWrapper f = f
   gaussWrapper = error "Cannot call gaussianDec for ZqBasic"
 
-instance (Storable a, Storable b, CRNS a, CRNS b, CRTrans a, CRTrans b) 
+instance (Storable a, Storable b, 
+          CRNS a, CRNS b, 
+          CRTrans a, CRTrans b, 
+          ZeroTestable a, ZeroTestable b, 
+          IntegralDomain a, IntegralDomain b,
+          Random a, Random b) 
   => CRNS (a,b) where
   zipWrapper f (CT' x :: CT' m (a,b)) (CT' y) =
     let (a,b) = unzip x
@@ -319,13 +327,13 @@
     (CT' b) <- gaussWrapper f
     return $ CT' $ zip a b
 
-mulGPow' :: (TElt CT r, Fact m) => CT' m r -> CT' m r
+mulGPow' :: (TElt CT r, Fact m, Additive r) => CT' m r -> CT' m r
 mulGPow' = lgWrapper $ untag $ lgDispatch dmulgpow
 
-divGPow' :: forall m r . (TElt CT r, Fact m) => CT' m r -> Maybe (CT' m r)
+divGPow' :: forall m r . (TElt CT r, Fact m, IntegralDomain r, ZeroTestable r) => CT' m r -> Maybe (CT' m r)
 divGPow' = divGWrapper $ untag $ checkDiv $ lgDispatch dginvpow
 
-crt' :: forall m r . (TElt CT r, Fact m, CRTrans r) 
+crt' :: forall m r . (TElt CT r, Fact m, CRTrans r, ZeroTestable r, IntegralDomain r) 
   => TaggedT m Maybe (CT' m r -> CT' m r)
 crt' = tagT $ crtWrapper $ do
   f <- proxyT ctCRT (Proxy::Proxy m)
@@ -500,7 +508,7 @@
         generate pp (\i -> wPow $ (-i*pow)))) $
       pureT ppsFact
 
-gCoeffsCRT, gInvCoeffsCRT :: (TElt CT r, CRTrans r, Fact m)
+gCoeffsCRT, gInvCoeffsCRT :: (TElt CT r, CRTrans r, Fact m, ZeroTestable r, IntegralDomain r)
   => TaggedT m Maybe (CT' m r)
 gCoeffsCRT = crt' <*> (return $ mulGPow' $ scalarPow' LP.one)
 -- It's necessary to call 'fromJust' here: otherwise 
@@ -519,7 +527,7 @@
 -- we can't put this in Extension with the rest of the twace/embed fucntions because it needs access to 
 -- the C backend
 twaceCRT' :: forall m m' r .
-             (TElt CT r, CRTrans r, m `Divides` m')
+             (TElt CT r, CRTrans r, m `Divides` m', ZeroTestable r, IntegralDomain r)
              => TaggedT '(m, m') Maybe (Vector r -> Vector r)
 twaceCRT' = tagT $ do -- Maybe monad
   (CT' g') <- proxyT gCoeffsCRT (Proxy::Proxy m')
diff --git a/src/Crypto/Lol/Cyclotomic/Tensor/RepaTensor.hs b/src/Crypto/Lol/Cyclotomic/Tensor/RepaTensor.hs
--- a/src/Crypto/Lol/Cyclotomic/Tensor/RepaTensor.hs
+++ b/src/Crypto/Lol/Cyclotomic/Tensor/RepaTensor.hs
@@ -75,12 +75,14 @@
 
 instance Tensor RT where
 
-  type TElt RT r = (IntegralDomain r, ZeroTestable r,
-                    Eq r, Random r, NFData r,
-                    Unbox r, Elt r)
+  type TElt RT r = (Unbox r, Elt r)
 
   entailIndexT  = tag $ Sub Dict
-  entailFullT   = tag $ Sub Dict
+  entailEqT = tag $ Sub Dict
+  entailZTT = tag $ Sub Dict
+  entailRingT = tag $ Sub Dict
+  entailNFDataT = tag $ Sub Dict
+  entailRandomT = tag $ Sub Dict
 
   scalarPow = RT . scalarPow'
 
diff --git a/src/Crypto/Lol/Cyclotomic/UCyc.hs b/src/Crypto/Lol/Cyclotomic/UCyc.hs
--- a/src/Crypto/Lol/Cyclotomic/UCyc.hs
+++ b/src/Crypto/Lol/Cyclotomic/UCyc.hs
@@ -28,7 +28,7 @@
 module Crypto.Lol.Cyclotomic.UCyc
 (
 -- * Data type
-  UCyc, CElt
+  UCyc, CElt, RElt
 -- * Basic operations
 , mulG, divG
 , scalarCyc, liftCyc
@@ -48,7 +48,7 @@
 import           Crypto.Lol.Cyclotomic.Tensor  as T
 import qualified Crypto.Lol.Cyclotomic.Utility as U
 import           Crypto.Lol.Gadget
-import           Crypto.Lol.LatticePrelude     as LP
+import           Crypto.Lol.LatticePrelude     as LP hiding ((*>))
 import           Crypto.Lol.Types.FiniteField
 import           Crypto.Lol.Types.ZPP
 
@@ -56,7 +56,7 @@
 import Algebra.Ring         as Ring (C)
 import Algebra.ZeroTestable as ZeroTestable (C)
 
-import Control.Applicative    hiding ((*>))
+import Control.Applicative
 import Control.DeepSeq
 import Control.Monad.Identity
 import Control.Monad.Random
@@ -67,7 +67,7 @@
 import Data.Typeable
 import Test.QuickCheck
 
-import qualified Debug.Trace as DT
+--import qualified Debug.Trace as DT
 
 -- | A data type for representing cyclotomic rings such as @Z[zeta]@,
 -- @Zq[zeta]@, and @Q(zeta)@: @t@ is the 'Tensor' type for storing
@@ -77,7 +77,7 @@
   Pow  :: !(t m r) -> UCyc t m r -- representation wrt powerful basis
   Dec  :: !(t m r) -> UCyc t m r -- decoding basis
 
-  -- Invariant: use CRTr if and only if crtFuncs exists for (t m r);
+  -- Invariant: use CRTr iff crtFuncs exists for (t m r);
   -- otherwise use CRTe (because crtFuncs is guaranteed to exist for
   -- (t m (CRTExt r))
   CRTr :: !(t m r) -> UCyc t m r -- wrt CRT basis over r, if it exists
@@ -96,15 +96,17 @@
 
 -- | Shorthand for frequently reused constraints that are needed for
 --  change of basis.
-type UCCtx t r = (Tensor t, CRTrans r, CRTrans (CRTExt r), CRTEmbed r,
-                  ZeroTestable r, TElt t r, TElt t (CRTExt r))
+type UCCtx t r = (Tensor t, RElt t r, RElt t (CRTExt r), CRTEmbed r)
 
--- | Shorthand for frequently reused constraints that are needed for
--- most functions involving 'UCyc' and 'Crypto.Lol.Cyclotomic.Cyc.Cyc'.
+-- | Collection of constraints need to work on most functions over a
+-- particular base ring @r@.
+type RElt t r = (TElt t r, CRTrans r, IntegralDomain r, ZeroTestable r, NFData r)
 
--- EAC: duplicated UCCtx for haddock
-type CElt t r = (Tensor t, CRTrans r, CRTrans (CRTExt r), CRTEmbed r,
-                 ZeroTestable r, TElt t r, TElt t (CRTExt r), Eq r, NFData r)
+-- | Shorthand for frequently reused constraints that are needed for
+-- most functions involving 'UCyc' and
+-- 'Crypto.Lol.Cyclotomic.Cyc.Cyc'.
+type CElt t r = (Tensor t, RElt t r, RElt t (CRTExt r),
+                 CRTEmbed r, Eq r, Random r)
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.scalarCyc', but for 'UCyc'.
 scalarCyc :: (Fact m, CElt t a) => a -> UCyc t m a
@@ -114,10 +116,11 @@
 instance (UCCtx t r, Fact m, Eq r) => Eq (UCyc t m r) where
   -- handle same bases when fidelity allows (i.e., *not* CRTe basis)
   (Scalar v1) == (Scalar v2) = v1 == v2
-  (Pow v1) == (Pow v2) = v1 == v2 \\ witness entailFullT v1
-  (Dec v1) == (Dec v2) = v1 == v2 \\ witness entailFullT v1
-  (CRTr v1) == (CRTr v2) = v1 == v2 \\ witness entailFullT v1
+  (Pow v1) == (Pow v2) = v1 == v2 \\ witness entailEqT v1
+  (Dec v1) == (Dec v2) = v1 == v2 \\ witness entailEqT v1
+  (CRTr v1) == (CRTr v2) = v1 == v2 \\ witness entailEqT v1
 
+  -- compare in compositum
   (Sub (c1 :: UCyc t l1 r)) == (Sub (c2 :: UCyc t l2 r)) =
     (embed' c1 :: UCyc t (FLCM l1 l2) r) == embed' c2
     \\ lcmDivides (Proxy::Proxy l1) (Proxy::Proxy l2)
@@ -131,9 +134,9 @@
 -- ZeroTestable instance
 instance (UCCtx t r, Fact m) => ZeroTestable.C (UCyc t m r) where
   isZero (Scalar v) = isZero v
-  isZero (Pow v) = isZero v \\ witness entailFullT v
-  isZero (Dec v) = isZero v \\ witness entailFullT v
-  isZero (CRTr v) = isZero v \\ witness entailFullT v
+  isZero (Pow v) = isZero v \\ witness entailZTT v
+  isZero (Dec v) = isZero v \\ witness entailZTT v
+  isZero (CRTr v) = isZero v \\ witness entailZTT v
   isZero x@(CRTe _) = isZero $ toPow' x
   isZero (Sub c) = isZero c
 
@@ -148,11 +151,10 @@
 
   -- SAME CONSTRUCTORS
   (Scalar c1) + (Scalar c2) = Scalar (c1+c2)
-  (Pow v1) + (Pow v2) = Pow $ v1 + v2 \\ witness entailFullT v1
-  (Dec v1) + (Dec v2) = Dec $ v1 + v2 \\ witness entailFullT v1
-  (CRTr v1) + (CRTr v2) = CRTr $ v1 + v2 \\ witness entailFullT v1
-  -- CJP: is this OK for precision?
-  (CRTe v1) + (CRTe v2) = CRTe $ v1 + v2 \\ witness entailFullT v1
+  (Pow v1) + (Pow v2) = Pow $ v1 + v2 \\ witness entailRingT v1
+  (Dec v1) + (Dec v2) = Dec $ v1 + v2 \\ witness entailRingT v1
+  (CRTr v1) + (CRTr v2) = CRTr $ v1 + v2 \\ witness entailRingT v1
+  (CRTe v1) + (CRTe v2) = CRTe $ v1 + v2 \\ witness entailRingT v1
   -- Sub plus Sub: work in compositum
   (Sub (c1 :: UCyc t m1 r)) + (Sub (c2 :: UCyc t m2 r)) =
     (Sub $ (embed' c1 :: UCyc t (FLCM m1 m2) r) + embed' c2)
@@ -164,15 +166,15 @@
   p1@(Scalar _) + p2@(Dec _) = toDec' p1 + p2
   p1@(Scalar _) + p2@(CRTr _) = toCRT' p1 + p2
   p1@(Scalar _) + p2@(CRTe _) = toCRT' p1 + p2
-  (Scalar v1) + (Sub c2) = Sub $ Scalar v1 + c2
+  (Scalar c1) + (Sub c2) = Sub $ Scalar c1 + c2 -- must re-wrap Scalar!
 
   p1@(Pow _) + p2@(Scalar _) = p1 + toPow' p2
   p1@(Dec _) + p2@(Scalar _) = p1 + toDec' p2
   p1@(CRTr _) + p2@(Scalar _) = p1 + toCRT' p2
   p1@(CRTe _) + p2@(Scalar _) = p1 + toCRT' p2
-  (Sub c1) + (Scalar v2) = Sub $ c1 + Scalar v2
+  (Sub c1) + (Scalar c2) = Sub $ c1 + Scalar c2
 
-  -- SUB PLUS SOMETHING ELSE (NON-SCALAR): work in full ring
+  -- SUB PLUS NON-SUB, NON-SCALAR: work in full ring
   (Sub c1) + c2 = embed' c1 + c2
   c1 + (Sub c2) = c1 + embed' c2
 
@@ -205,36 +207,35 @@
   _ * v2@(Scalar c2) | isZero c2 = v2
 
   -- BOTH IN A CRT BASIS
-  (CRTr v1) * (CRTr v2) = CRTr $ v1 * v2 \\ witness entailFullT v1
-  (CRTe v1) * (CRTe v2) = toPow' $ CRTe $ v1 * v2 \\ witness entailFullT v1
+  (CRTr v1) * (CRTr v2) = CRTr $ v1 * v2 \\ witness entailRingT v1
+  (CRTe v1) * (CRTe v2) = toPow' $ CRTe $ v1 * v2 \\ witness entailRingT v1
 
+  -- CRTr/CRTe mixture
+  (CRTr _) * (CRTe _) = error "UCyc.(*): mixed CRTr/CRTe"
+  (CRTe _) * (CRTr _) = error "UCyc.(*): mixed CRTr/CRTe"
+
   -- AT LEAST ONE SCALAR
   (Scalar c1) * (Scalar c2) = Scalar $ c1 * c2
 
   (Scalar c) * (Pow v) = Pow $ fmapT (*c) v
   (Scalar c) * (Dec v) = Dec $ fmapT (*c) v
   (Scalar c) * (CRTr v) = CRTr $ fmapT (*c) v
-  s@(Scalar _) * c'@(CRTe _) = s * toPow' c'
-  (Scalar c) * (Sub c2) = Sub $ Scalar c * c2
+  (Scalar c) * (CRTe v) = CRTe $ fmapT (* toExt c) v
+  (Scalar c1) * (Sub c2) = Sub $ Scalar c1 * c2
 
   (Pow v) * (Scalar c) = Pow $ fmapT (*c) v
   (Dec v) * (Scalar c) = Dec $ fmapT (*c) v
   (CRTr v) * (Scalar c) = CRTr $ fmapT (*c) v
-  c'@(CRTe _) * s@(Scalar _) = toPow' c' * s
-  (Sub c1) * (Scalar c) = Sub $ c1 * Scalar c
-
-  -- AT LEAST ONE SUB
+  (CRTe v) * (Scalar c) = CRTe $ fmapT (* toExt c) v
+  (Sub c1) * (Scalar c2) = Sub $ c1 * Scalar c2
 
-  -- two Subs: work in compositum
+  -- TWO SUBS: work in a CRT rep for compositum
   (Sub (c1 :: UCyc t m1 r)) * (Sub (c2 :: UCyc t m2 r)) =
-    (Sub $ (embed' c1 :: UCyc t (FLCM m1 m2) r) * embed' c2)
+    -- re-wrap c1, c2 as Subs of the composition, and force them to CRT
+    (Sub $ (toCRT' $ Sub c1 :: UCyc t (FLCM m1 m2) r) * toCRT' (Sub c2))
     \\ lcm2Divides (Proxy::Proxy m1) (Proxy::Proxy m2) (Proxy::Proxy m)
 
-  -- Sub times something else (non-Scalar): work in full ring
-  (Sub c1) * p2 = embed' c1 * p2
-  p1 * (Sub c2) = p1 * embed' c2
-
-  -- ELSE: work in appropriate CRT basis
+  -- ELSE: work in appropriate CRT rep
   p1 * p2 = toCRT' p1 * toCRT' p2
 
   fromInteger = Scalar . fromInteger
@@ -243,7 +244,10 @@
 instance (Reduce a b, Fact m, CElt t a, CElt t b)
   => Reduce (UCyc t m a) (UCyc t m b) where
 
-  reduce = fmapC reduce . forceAny
+  -- optimized for subring constructors
+  reduce (Scalar c) = Scalar $ reduce c
+  reduce (Sub (c :: UCyc t l a)) = Sub (reduce c :: UCyc t l b)
+  reduce x = fmapC reduce $ forceAny x
 
 -- promote Gadget from base ring
 instance (Gadget gad zq, Fact m, CElt t zq) => Gadget gad (UCyc t m zq) where
@@ -252,14 +256,20 @@
   encode s = ((* adviseCRT s) <$>) <$> gadget
 
 -- promote Decompose, using the powerful basis
-instance (Decompose gad zq, Fact m, CElt t zq,
-          Reduce (UCyc t m (DecompOf zq)) (UCyc t m zq))
+instance (Decompose gad zq, Fact m,
+         -- these imply (superclass) Reduce on UCyc; needed for Sub case
+          CElt t zq, CElt t (DecompOf zq), Reduce (DecompOf zq) zq)
   => Decompose gad (UCyc t m zq) where
 
   type DecompOf (UCyc t m zq) = UCyc t m (DecompOf zq)
 
+  -- faster implementations: decompose directly in subring, which is
+  -- correct because we decompose in powerful basis
+  decompose (Scalar c) = pasteT $ Scalar <$> peelT (decompose c)
+  decompose (Sub c) = pasteT $ Sub <$> peelT (decompose c)
+
   -- traverse: Traversable (c m) and Applicative (Tagged gad ZL)
-  decompose = fromZL . traverse (toZL . decompose) . forcePow
+  decompose x = fromZL $ traverse (toZL . decompose) $ forcePow x
     where toZL :: Tagged s [a] -> TaggedT s ZipList a
           toZL = coerce
           fromZL :: TaggedT s ZipList a -> Tagged s [a]
@@ -269,35 +279,55 @@
 instance (Correct gad zq, Fact m, CElt t zq)
          => Correct gad (UCyc t m zq) where
   -- sequenceA: Applicative (c m) and Traversable (TaggedT [])
-  correct bs = (correct . pasteT) <$> (sequenceA $ forceDec <$> peelT bs)
+  correct bs = (correct . pasteT) <$> sequenceA (forceDec <$> peelT bs)
 
 -- generic RescaleCyc instance
 
 instance {-# OVERLAPS #-} (Rescale a b, CElt t a, CElt t b)
          => U.RescaleCyc (UCyc t) a b where
-  rescaleCyc b = fmapC rescale . forceBasis (Just b)
 
+  -- Optimized for subring constructors, for powerful basis.
+  -- Analogs for decoding basis are not quite correct, because (* -1)
+  -- doesn't commute with 'rescale' due to tiebreakers!
+  rescaleCyc U.Pow (Scalar c) = Scalar $ rescale c
+  rescaleCyc U.Pow (Sub (c :: UCyc t l a)) =
+    Sub (U.rescaleCyc U.Pow c :: UCyc t l b)
+
+  rescaleCyc b x = fmapC rescale $ forceBasis (Just b) x
+
 -- specialized instance for product rings: ~2x faster algorithm
-instance (Mod a, Field b, Lift a z, Reduce z b,
-          CElt t a, CElt t b, CElt t (a,b), CElt t z)
+instance (Mod a, Field b, Lift a (ModRep a), Reduce (LiftOf a) b,
+          CElt t a, CElt t b, CElt t (a,b), CElt t (LiftOf a))
          => U.RescaleCyc (UCyc t) (a,b) b where
-  rescaleCyc bas =
+
+  -- optimized for subrings and powerful basis (see comments in other
+  -- instance for why this doesn't work for decoding basis)
+  rescaleCyc U.Pow (Scalar c) = Scalar $ rescale c
+  rescaleCyc U.Pow (Sub (c :: UCyc t l (a,b))) =
+    Sub (U.rescaleCyc U.Pow c :: UCyc t l b)
+
+  rescaleCyc bas x =
     let aval = proxy modulus (Proxy::Proxy a)
   -- CJP: could use unzipC here to get (a,b) in one pass, but it
   -- requires adding that method, and unzipT to Tensor and all its
   -- instances. Probably not worth it.
-    in \x -> let y = forceAny x
-                 a = fmapC fst y
-                 b = fmapC snd y
-                 z = liftCyc bas a
-             in (pure (recip (fromIntegral aval))) * (b - reduce z)
+        y = forceAny x
+        a = fmapC fst y
+        b = fmapC snd y
+        z = liftCyc bas a
+    in Scalar (recip (reduce aval)) * (b - reduce z)
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.liftCyc', but for 'UCyc'.
 liftCyc :: (Lift b a, Fact m, CElt t a, CElt t b)
            => U.Basis -> UCyc t m b -> UCyc t m a
-liftCyc U.Pow = fmapC lift . forceBasis (Just U.Pow)
-liftCyc U.Dec = fmapC lift . forceBasis (Just U.Dec)
+-- optimized for subrings and powerful basis (see comments in
+-- RescaleCyc instances for why this doesn't work for decoding)
+liftCyc U.Pow (Scalar c) = Scalar $ lift c
+liftCyc U.Pow (Sub c) = Sub $ liftCyc U.Pow c
 
+liftCyc U.Pow x = fmapC lift $ forceBasis (Just U.Pow) x
+liftCyc U.Dec x = fmapC lift $ forceBasis (Just U.Dec) x
+
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.adviseCRT', but for 'UCyc'.
 adviseCRT :: (Fact m, CElt t r) => UCyc t m r -> UCyc t m r
 adviseCRT x@(Scalar _) = x
@@ -310,9 +340,9 @@
 mulG (Sub c) = mulG $ embed' c                -- must go to full ring
 mulG (Pow v) = Pow $ mulGPow v
 mulG (Dec v) = Dec $ mulGDec v
--- fromJust is safe here because we're already in CRTr
-mulG (CRTr v) = CRTr $ fromMaybe (error "FC.mulG CRTr") mulGCRT v
-mulG (CRTe v) = CRTe $ fromMaybe (error "FC.mulG CRTe") mulGCRT v
+-- fromMaybe is safe here because we're already in CRTr
+mulG (CRTr v) = CRTr $ fromJust' "UCyc.mulG CRTr" mulGCRT v
+mulG (CRTe v) = CRTe $ fromJust' "UCyc.mulG CRTe" mulGCRT v
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.divG', but for 'UCyc'.
 divG :: (Fact m, CElt t r) => UCyc t m r -> Maybe (UCyc t m r)
@@ -320,9 +350,9 @@
 divG (Sub c) = divG $ embed' c                      -- full ring
 divG (Pow v) = Pow <$> divGPow v
 divG (Dec v) = Dec <$> divGDec v
--- fromJust is safe here because we're already in CRTr
-divG (CRTr v) = Just $ CRTr $ fromMaybe (error "FC.divG CRTr") divGCRT v
-divG (CRTe v) = Just $ CRTe $ fromMaybe (error "FC.divG CRTe") divGCRT v
+-- fromMaybe is safe here because we're already in CRTr
+divG (CRTr v) = Just $ CRTr $ fromJust' "UCyc.divG CRTr" divGCRT v
+divG (CRTe v) = Just $ CRTe $ fromJust' "UCyc.divG CRTe" divGCRT v
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.tGaussian', but for 'UCyc'.
 tGaussian :: (Fact m, OrdFloat q, Random q, CElt t q,
@@ -334,7 +364,7 @@
 errorRounded :: forall v rnd t m z .
                 (ToInteger z, Fact m, CElt t z, ToRational v, MonadRandom rnd)
                 => v -> rnd (UCyc t m z)
-errorRounded svar = 
+errorRounded svar =
   fmapC (roundMult one) <$> (tGaussian svar :: rnd (UCyc t m Double))
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.errorCoset', but for 'UCyc'.
@@ -373,14 +403,17 @@
   \\ gcdDivides (Proxy::Proxy l) (Proxy::Proxy m)
 twace (Pow v) = Pow $ twacePowDec v
 twace (Dec v) = Dec $ twacePowDec v
--- stay in CRTr only if it's possible, otherwise go to Pow
+-- stay in CRTr only iff it's valid for target, else go to Pow
 twace x@(CRTr v) =
   fromMaybe (twace $ toPow' x) (CRTr <$> (twaceCRT <*> pure v))
--- CJP: stay in CRTe: precision OK?
-twace (CRTe v) = CRTe $ fromMaybe (error "FC.twace CRTe") twaceCRT v
+-- stay in CRTe iff CRTr is invalid for target, else go to Pow
+twace x@(CRTe v) =
+  fromMaybe (CRTe $ fromJust' "UCyc.twace CRTe" twaceCRT v)
+            (proxy (pasteT hasCRTFuncs) (Proxy::Proxy (t m r)) *>
+             pure (twace $ toPow' x))
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.coeffsCyc', but for 'UCyc'.
-coeffsCyc :: (m `Divides` m', CElt t r) 
+coeffsCyc :: (m `Divides` m', CElt t r)
              => U.Basis -> UCyc t m' r -> [UCyc t m r]
 coeffsCyc U.Pow (Pow v) = LP.map Pow $ coeffs v
 coeffsCyc U.Dec (Dec v) = LP.map Dec $ coeffs v
@@ -393,7 +426,7 @@
 
 -- | Same as 'Crypto.Lol.Cyclotomic.Cyc.crtSet', but for 'UCyc'.
 crtSet :: forall t m m' r p mbar m'bar .
-           (m `Divides` m', ZPP r, p ~ CharOf (ZPOf r), 
+           (m `Divides` m', ZPP r, p ~ CharOf (ZPOf r),
             mbar ~ PFree p m, m'bar ~ PFree p m',
             CElt t r, CElt t (ZPOf r))
            => Tagged m [UCyc t m' r]
@@ -422,6 +455,7 @@
 forceBasis (Just U.Pow) x = toPow' x
 forceBasis (Just U.Dec) x = toDec' x
 forceBasis Nothing x@(Scalar _) = toPow' x
+-- force as outermost op to ensure we get an r-basis
 forceBasis Nothing (Sub c) = forceBasis Nothing $ embed' c
 forceBasis Nothing x@(CRTe _) = toPow' x
 forceBasis Nothing x = x
@@ -470,20 +504,21 @@
 
 ---------- HELPER FUNCTIONS (NOT FOR EXPORT) ----------
 
--- | Force embed, to a non-Sub constructor.
+-- | Force embed, to a non-'Sub' constructor.  Preserves Scalar, Pow,
+-- Dec constructors, and CRTr/CRTe constructor if valid in both source
+-- and target ring (we rely on this in toCRT').
 embed' :: forall t r l m .
           (UCCtx t r, l `Divides` m) => UCyc t l r -> UCyc t m r
-embed' (Scalar v) = Scalar v
+embed' (Scalar x) = Scalar x    -- must re-wrap!
 embed' (Pow v) = Pow $ embedPow v
 embed' (Dec v) = Dec $ embedDec v
 -- stay in CRTr only if it's possible, otherwise go to Pow
 embed' x@(CRTr v) =
     fromMaybe (embed' $ toPow' x) (CRTr <$> (embedCRT <*> pure v))
--- Staying in CRTe might not be safe, because the target tensor
--- might have implemented a CRTr even if the source tensor
--- hasn't.  Mathematically this is impossible (because target has
--- CRTr only if source does), so this is purely about implementation.
-embed' x@(CRTe _) = embed' $ toPow' x
+embed' x@(CRTe v) = -- go to CRTe iff CRTr is invalid for target index
+    fromMaybe (CRTe $ fromJust' "UCyc.embed' CRTe" embedCRT v)
+              (proxy (pasteT hasCRTFuncs) (Proxy::Proxy (t m r)) *>
+               pure (embed' $ toPow' x))
 embed' (Sub (c :: UCyc t k r)) = embed' c
   \\ transDivides (Proxy::Proxy k) (Proxy::Proxy l) (Proxy::Proxy m)
 
@@ -493,57 +528,68 @@
 toPow', toDec' :: (UCCtx t r, Fact m) => UCyc t m r -> UCyc t m r
 -- forces the argument into the powerful basis
 toPow' (Scalar c) = Pow $ scalarPow c
-toPow' (Sub c) = toPow' $ embed' c
+toPow' (Sub c) = embed' $ toPow' c -- OK: embed' preserves Pow
 toPow' x@(Pow _) = x
 toPow' (Dec v) = Pow $ l v
-toPow' (CRTr v) = Pow $ fromMaybe (error "FC.toPow'") crtInv v
-toPow' (CRTe v) = Pow $ fmapT fromExt $ fromMaybe (error "FC.toPow'") crtInv v
+toPow' (CRTr v) = Pow $ fromJust' "UCyc.toPow'" crtInv v
+toPow' (CRTe v) =
+    Pow $ fmapT fromExt $ fromJust' "UCyc.toPow' CRTe" crtInv v
 
--- forces the argument into the decoding basis
-toDec' x@(Scalar _) = toDec' $ toPow' x -- use scalarDec instead
-toDec' (Sub c) = toDec' $ embed' c
+-- | Force the argument into the decoding basis.
+toDec' x@(Scalar _) = toDec' $ toPow' x -- TODO: use scalarDec instead
+toDec' (Sub c) = embed' $ toDec' c      -- OK: embed' preserves Dec
 toDec' (Pow v) = Dec $ lInv v
 toDec' x@(Dec _) = x
-toDec' (CRTr v) = Dec $ lInv $ fromMaybe (error "FC.toDec'") crtInv v
-toDec' (CRTe v) = Dec $ lInv $ fmapT fromExt $ fromMaybe (error "FC.toDec'") crtInv v
+toDec' x@(CRTr _) = toDec' $ toPow' x
+toDec' x@(CRTe _) = toDec' $ toPow' x
 
--- forces the argument into a CRT basis, according to the invariant
--- about which one should be used
+-- | Force the argument into the "valid" CRT basis for our invariant.
 toCRT' :: forall t m r . (UCCtx t r, Fact m) => UCyc t m r -> UCyc t m r
-toCRT' (Sub c) = toCRT' $ embed' c
 toCRT' x@(CRTr _) = x
 toCRT' x@(CRTe _) = x
+toCRT' (Sub (c :: UCyc t l r)) =
+    case (proxyT hasCRTFuncs (Proxy::Proxy (t l r)),
+          proxyT hasCRTFuncs (Proxy::Proxy (t m r))) of
+      (Just _, Just _) -> embed' $ toCRT' c -- fastest; embed' preserves CRTr
+      (_, Nothing) -> embed' $ toCRTe c -- faster; temp violate CRTr/e invariant
+      _ -> toCRT' $ embed' c            -- fallback
 toCRT' x = fromMaybe (toCRTe x) (toCRTr <*> pure x)
-  -- CJP: defining these helpers internally so they can't be called
-  -- from anywhere else.  Therefore, the only way to convert to a
-  -- CRT basis is through the toCRT' method.
-  where
-    toCRTr = do -- Maybe monad
-      crt' <- crt
-      scalarCRT' <- scalarCRT
-      return $ \x -> case x of
-        (Scalar c) -> CRTr $ scalarCRT' c
-        (Pow v) -> CRTr $ crt' v
-        (Dec v) -> CRTr $ crt' $ l v
-          -- deliberately omit CRTe case, which should
-          -- never happen by internal invariant, so trigger
-          -- error if it does
-    toCRTe = let m = proxy valueFact (Proxy::Proxy m)
-                 crt' = fromMaybe (error $ "FC.toCRT': no crt': " ++ (show m)) crt :: t m (CRTExt r) -> t m (CRTExt r) -- must exist
-                 scalarCRT' = fromMaybe (error "FC.toCRT': no scalar crt'") scalarCRT :: CRTExt r -> t m (CRTExt r)
-             in \x -> case x of
-               (Scalar c) -> CRTe $ scalarCRT' $ toExt c
-               (Pow v) -> CRTe $ crt' $ fmapT toExt v
-               (Dec v) -> CRTe $ crt' $ fmapT toExt $ l v
 
+toCRTr :: forall t m r . (UCCtx t r, Fact m) => Maybe (UCyc t m r -> UCyc t m r)
+toCRTr = do -- Maybe monad
+  crt' <- crt
+  scalarCRT' <- scalarCRT
+  return $ \x -> case x of
+                   (Scalar c) -> CRTr $ scalarCRT' c
+                   (Pow v) -> CRTr $ crt' v
+                   (Dec v) -> CRTr $ crt' $ l v
+                   c@(CRTr _) -> c
+                   c@(CRTe _) -> fromJust' "UCyc.toCRTr CRTe" toCRTr $ toPow' c
+                   (Sub _) -> error "UCyc.toCRTr: Sub"
+
+toCRTe :: forall t m r . (UCCtx t r, Fact m) => UCyc t m r -> UCyc t m r
+toCRTe = let m = proxy valueFact (Proxy::Proxy m)
+             crt' = fromJust' ("UCyc.toCRTe: no crt': " ++ show m) crt
+                  :: t m (CRTExt r) -> t m (CRTExt r) -- must exist
+             scalarCRT' = fromJust' "UCyc.toCRTe: no scalarCRT" scalarCRT
+                        :: CRTExt r -> t m (CRTExt r)
+         in \x -> case x of
+                    (Scalar c) -> CRTe $ scalarCRT' $ toExt c
+                    (Pow v) -> CRTe $ crt' $ fmapT toExt v
+                    (Dec v) -> CRTe $ crt' $ fmapT toExt $ l v
+                    c@(CRTr _) -> toCRTe $ toPow' c
+                    c@(CRTe _) -> c
+                    (Sub _) -> error "UCyc.toCRTe: Sub"
+
 ---------- "Container" instances ----------
 
 instance (Tensor t, Fact m) => Functor (UCyc t m) where
   -- Functor instance is implied by Applicative laws
   fmap f x = pure f <*> x
 
+errApp :: String -> a
 errApp name = error $ "UCyc.Applicative: can't/won't handle " ++ name ++
-              "; call forcePow|Dec first"
+              "; call forcePow|Dec|Any first"
 
 instance (Tensor t, Fact m) => Applicative (UCyc t m) where
 
@@ -595,12 +641,11 @@
   (CRTr v) <*> (Scalar a) = CRTr $ v <*> pure a \\ witness entailIndexT v
 
   -- cases we can't/won't handle
-  (Pow _) <*> (Dec _) = error "UCyc.Applicative: Pow/Dec combo"
-  (Dec _) <*> (Pow _) = error "UCyc.Applicative: Pow/Dec combo"
   (Sub _) <*> _  = errApp "Sub"
   _ <*> (Sub _)  = errApp "Sub"
   (CRTe _) <*> _ = errApp "CRTe"
   _ <*> (CRTe _) = errApp "CRTe"
+  _ <*> _ = errApp "mismatched Pow/Dec/CRTr bases"
 
 instance (Tensor t, Fact m) => Foldable (UCyc t m) where
   foldr f b (Scalar r) = f r b
@@ -620,13 +665,13 @@
 
 ---------- Utility instances ----------
 
-instance (Tensor t, Fact m, TElt t r, CRTrans r) => Random (UCyc t m r) where
+instance (Tensor t, Fact m, TElt t r, CRTrans r, Random r, ZeroTestable r, IntegralDomain r) => Random (UCyc t m r) where
 
   -- create in CRTr basis if legal, otherwise in powerful
   random = let cons = fromMaybe Pow
                       (proxyT hasCRTFuncs (Proxy::Proxy (t m r)) >> Just CRTr)
            in \g -> let (v,g') = random g
-                                 \\ proxy entailFullT (Proxy::Proxy (t m r))
+                                 \\ proxy entailRandomT (Proxy::Proxy (t m r))
                     in (cons v, g')
 
   randomR _ = error "randomR non-sensical for cyclotomic rings"
@@ -645,11 +690,11 @@
   arbitrary = liftM Pow arbitrary
   shrink = shrinkNothing
 
-instance (Tensor t, Fact m, NFData r, TElt t r, TElt t (CRTExt r))
+instance (Tensor t, Fact m, TElt t r, TElt t (CRTExt r), NFData r, NFData (CRTExt r))
          => NFData (UCyc t m r) where
-  rnf (Pow x)    = rnf x \\ witness entailFullT x
-  rnf (Dec x)    = rnf x \\ witness entailFullT x
-  rnf (CRTr x)   = rnf x \\ witness entailFullT x
-  rnf (CRTe x)   = rnf x \\ witness entailFullT x
+  rnf (Pow x)    = rnf x \\ witness entailNFDataT x
+  rnf (Dec x)    = rnf x \\ witness entailNFDataT x
+  rnf (CRTr x)   = rnf x \\ witness entailNFDataT x
+  rnf (CRTe x)   = rnf x \\ witness entailNFDataT x
   rnf (Scalar x) = rnf x
   rnf (Sub x)    = rnf x
diff --git a/src/Crypto/Lol/GaussRandom.hs b/src/Crypto/Lol/GaussRandom.hs
--- a/src/Crypto/Lol/GaussRandom.hs
+++ b/src/Crypto/Lol/GaussRandom.hs
@@ -26,7 +26,13 @@
     in do (u,v) <- iterateWhile uvGuard getUV
           let t = u*u+v*v
               com = sqrt (-var * log t / t)
-          return (u * com, v * com)
+          -- we can either sample u,v from [-1,1]
+          -- or generate sign bits for the outputs
+          s1 <- getRandom
+          s2 <- getRandom
+          let u' = if s1 then u else -u
+              v' = if s2 then v else -v
+          return (u'*com,v'*com)
     where getUV = do u <- getRandomR (zero,one)
                      v <- getRandomR (zero,one)
                      return (u,v)
diff --git a/src/Crypto/Lol/LatticePrelude.hs b/src/Crypto/Lol/LatticePrelude.hs
--- a/src/Crypto/Lol/LatticePrelude.hs
+++ b/src/Crypto/Lol/LatticePrelude.hs
@@ -24,7 +24,7 @@
 , module Crypto.Lol.Factored
 -- * Miscellaneous
 , rescaleMod, roundCoset
-, pureT, peelT, pasteT, withWitness, withWitnessT
+, fromJust', pureT, peelT, pasteT, withWitness, withWitnessT
 , module Data.Functor.Trans.Tagged
 , module Data.Proxy
 ) where
@@ -221,6 +221,10 @@
   randomR ((loa,lob), (hia,hib)) g = let (a,g') = randomR (loa,hia) g
                                          (b,g'') = randomR (lob,hib) g'
                                      in ((a,b),g'')
+
+-- | Version of 'fromJust' with an error message.
+fromJust' :: String -> Maybe a -> a
+fromJust' str = fromMaybe (error str)
 
 -- | Apply any applicative to a Tagged value.
 pureT :: Applicative f => TaggedT t Identity a -> TaggedT t f a
diff --git a/test-suite/TensorTests.hs b/test-suite/TensorTests.hs
--- a/test-suite/TensorTests.hs
+++ b/test-suite/TensorTests.hs
@@ -47,13 +47,14 @@
    ]
 
 
-type TMRCtx t m r = (Tensor t, Fact m, m `Divides` m, CRTrans r, TElt t r, CRTEmbed r, TElt t (CRTExt r))
+type TMRCtx t m r = (Tensor t, Fact m, m `Divides` m, CRTrans r, TElt t r, CRTEmbed r, 
+                     TElt t (CRTExt r), Eq r, ZeroTestable r, IntegralDomain r)
 
 prop_fmap :: (TMRCtx t m r) => t m r -> Bool
-prop_fmap x = fmapT id x == x \\ witness entailFullT x \\ witness entailIndexT x
+prop_fmap x = fmapT id x == x \\ witness entailEqT x \\ witness entailIndexT x
 
 prop_fmap2 :: (TMRCtx t m r) => t m r -> Bool
-prop_fmap2 x = (fmapT id x) == (fmap id x) \\ witness entailFullT x \\ witness entailIndexT x
+prop_fmap2 x = (fmapT id x) == (fmap id x) \\ witness entailEqT x \\ witness entailIndexT x
 
 -- tests that multiplication in the extension ring matches CRT multiplication
 prop_mul_ext :: forall t m r . (TMRCtx t m r)
@@ -64,7 +65,10 @@
        Nothing -> error "mul have a CRT to call prop_mul_ext"
        Just _ -> (let z = x * y
                       z' = fmapT fromExt $ (fmapT toExt x) * (fmapT toExt y)
-                  in z == z') \\ witness entailFullT x \\ witness entailFullT (fmap toExt x) \\ witness entailIndexT x
+                  in z == z') \\ witness entailEqT x 
+                              \\ witness entailRingT x
+                              \\ witness entailRingT (fmap toExt x)
+                              \\ witness entailIndexT x
 
 gInvGTests = testGroup "GInv.G == id" [
   testGroup "Pow basis" $ groupTMR $ wrapTmrToBool prop_ginv_pow,
@@ -74,30 +78,30 @@
 -- divG . mulG == id in Pow basis
 prop_ginv_pow :: (TMRCtx t m r) => t m r -> Bool
 prop_ginv_pow x = (fromMaybe (error "could not divide by G in prop_ginv_pow") $ 
-  divGPow $ mulGPow x) == x \\ witness entailFullT x
+  divGPow $ mulGPow x) == x \\ witness entailEqT x
 
 -- divG . mulG == id in Dec basis
 prop_ginv_dec :: (TMRCtx t m r) => t m r -> Bool
 prop_ginv_dec x = (fromMaybe (error "could not divide by G in prop_ginv_dec") $ 
-  divGDec $ mulGDec x) == x \\ witness entailFullT x
+  divGDec $ mulGDec x) == x \\ witness entailEqT x
 
 -- divG . mulG == id in CRT basis
 prop_ginv_crt :: (TMRCtx t m r) => t m r -> Bool
 prop_ginv_crt x = fromMaybe (error "no CRT in prop_ginv_crt") $ do
   divGCRT' <- divGCRT
   mulGCRT' <- mulGCRT
-  return $ (divGCRT' $ mulGCRT' x) == x \\ witness entailFullT x
+  return $ (divGCRT' $ mulGCRT' x) == x \\ witness entailEqT x
 
 -- crtInv . crt == id
 prop_crt_inv :: (TMRCtx t m r) => t m r -> Bool
 prop_crt_inv x = fromMaybe (error "no CRT in prop_crt_inv") $ do
   crt' <- crt
   crtInv' <- crtInv
-  return $ (crtInv' $ crt' x) == x \\ witness entailFullT x
+  return $ (crtInv' $ crt' x) == x \\ witness entailEqT x
 
 -- lInv . l == id
 prop_l_inv :: (TMRCtx t m r) => t m r -> Bool
-prop_l_inv x = (lInv $ l x) == x \\ witness entailFullT x
+prop_l_inv x = (lInv $ l x) == x \\ witness entailEqT x
 
 -- scalarCRT = crt . scalarPow
 prop_scalar_crt :: forall t m r . (TMRCtx t m r)
@@ -106,7 +110,7 @@
   scalarCRT' <- scalarCRT
   crt' <- crt
   return $ (scalarCRT' r :: t m r) == (crt' $ scalarPow r)
-  \\ proxy entailFullT (Proxy::Proxy (t m r))
+  \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 gCommuteTests = testGroup "G commutes with L" [
   testGroup "Dec basis" $ groupTMR $ wrapTmrToBool prop_g_dec,
@@ -114,14 +118,14 @@
 
 -- mulGDec == lInv. mulGPow . l
 prop_g_dec :: (TMRCtx t m r) => t m r -> Bool
-prop_g_dec x = (mulGDec x) == (lInv $ mulGPow $ l x) \\ witness entailFullT x
+prop_g_dec x = (mulGDec x) == (lInv $ mulGPow $ l x) \\ witness entailEqT x
 
 prop_g_crt :: (TMRCtx t m r) => t m r -> Bool
 prop_g_crt x = fromMaybe (error "no CRT in prop_g_crt") $ do
   mulGCRT' <- mulGCRT
   crt' <- crt
   crtInv' <- crtInv
-  return $ (mulGCRT' x) == (crt' $ mulGPow $ crtInv' x) \\ witness entailFullT x
+  return $ (mulGCRT' x) == (crt' $ mulGPow $ crtInv' x) \\ witness entailEqT x
 
 type TMRWrapCtx t m r = (TMRCtx t m r, Show (t m r), Arbitrary (t m r), Show r, Arbitrary r)
 
@@ -192,7 +196,7 @@
 
 
 
-type TMM'RCtx t m m' r = (Tensor t, m `Divides` m', TElt t r, Ring r, CRTrans r)
+type TMM'RCtx t m m' r = (Tensor t, m `Divides` m', TElt t r, Ring r, CRTrans r, Eq r, ZeroTestable r, IntegralDomain r)
 
 -- groups related tests
 tremTests = testGroup "Tr.Em == id" [
@@ -203,18 +207,18 @@
 -- tests that twace . embed == id in the Pow basis
 prop_trem_pow :: forall t m m' r . (TMM'RCtx t m m' r)
   => Proxy m' -> t m r -> Bool
-prop_trem_pow _ x = (twacePowDec $ (embedPow x :: t m' r)) == x \\ witness entailFullT x
+prop_trem_pow _ x = (twacePowDec $ (embedPow x :: t m' r)) == x \\ witness entailEqT x
 
 -- tests that twace . embed == id in the Dec basis
 prop_trem_dec :: forall t m m' r . (TMM'RCtx t m m' r)
   => Proxy m' -> t m r -> Bool
-prop_trem_dec _ x = (twacePowDec $ (embedDec x :: t m' r)) == x \\ witness entailFullT x
+prop_trem_dec _ x = (twacePowDec $ (embedDec x :: t m' r)) == x \\ witness entailEqT x
 
 -- tests that twace . embed == id in the CRT basis
 prop_trem_crt :: forall t m m' r . (TMM'RCtx t m m' r)
   => Proxy m' -> t m r -> Bool
 prop_trem_crt _ x = fromMaybe (error "no CRT in prop_trem_crt") $
-  (x==) <$> (twaceCRT <*> (embedCRT <*> pure x :: Maybe (t m' r))) \\ witness entailFullT x
+  (x==) <$> (twaceCRT <*> (embedCRT <*> pure x :: Maybe (t m' r))) \\ witness entailEqT x
 
 embedCommuteTests = testGroup "Em commutes with L" [
   testGroup "Dec basis" $ groupTMM'R $ wrapTmm'rToBool prop_embed_dec,
@@ -223,7 +227,7 @@
 -- embedDec == lInv . embedPow . l
 prop_embed_dec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> t m r -> Bool
 prop_embed_dec _ x = (embedDec x :: t m' r) == (lInv $ embedPow $ l x) 
-  \\ proxy entailFullT (Proxy::Proxy (t m' r))
+  \\ proxy entailEqT (Proxy::Proxy (t m' r))
 
 -- embedCRT = crt . embedPow . crtInv
 prop_embed_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> t m r -> Bool
@@ -232,7 +236,7 @@
   crtInv' <- crtInv
   embedCRT' <- embedCRT
   return $ (embedCRT' x :: t m' r) == (crt' $ embedPow $ crtInv' x) 
-    \\ proxy entailFullT (Proxy::Proxy (t m' r))
+    \\ proxy entailEqT (Proxy::Proxy (t m' r))
 
 twaceCommuteTests = testGroup "Tw commutes with L" [
   testGroup "Dec basis" $ groupTMM'R $ wrapTm'mrToBool prop_twace_dec,
@@ -241,7 +245,7 @@
 -- twacePowDec = lInv . twacePowDec . l
 prop_twace_dec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m -> t m' r -> Bool
 prop_twace_dec _ x = (twacePowDec x :: t m r) == (lInv $ twacePowDec $ l x)
-  \\ proxy entailFullT (Proxy::Proxy (t m r))
+  \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 -- twaceCRT = crt . twacePowDec . crtInv
 prop_twace_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m -> t m' r -> Bool
@@ -250,7 +254,7 @@
   crt' <- crt
   crtInv' <- crtInv
   return $ (twaceCRT' x :: t m r) == (crt' $ twacePowDec $ crtInv' x)
-    \\ proxy entailFullT (Proxy::Proxy (t m r))
+    \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 twaceInvarTests = testGroup "Twace invariants" [
   testGroup "Tw and Em ID for equal indices" $ groupTMR $ wrapTmrToBool $ prop_twEmID,
@@ -261,12 +265,12 @@
   testGroup "Invar2 CRT basis" $ groupTMM'R $ wrapProxyTmm'rToBool prop_twace_invar2_crt
   ]
 
-prop_twEmID :: forall t m r . (Tensor t, TElt t r, CRTrans r, Fact m, m `Divides` m) => t m r -> Bool
+prop_twEmID :: forall t m r . (Tensor t, TElt t r, CRTrans r, Fact m, m `Divides` m, Eq r, ZeroTestable r, IntegralDomain r) => t m r -> Bool
 prop_twEmID x = ((twacePowDec x) == x) &&
                   (((fromMaybe (error "twemid_crt") twaceCRT) x) == x) &&
                   ((embedPow x) == x) &&
                   ((embedDec x) == x) &&
-                  (((fromMaybe (error "twemid_crt") embedCRT) x) == x) \\ witness entailFullT x
+                  (((fromMaybe (error "twemid_crt") embedCRT) x) == x) \\ witness entailEqT x
 
 -- twace mhat'/g' = mhat*totm'/totm/g (Pow basis)
 prop_twace_invar1_pow :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool
@@ -277,7 +281,7 @@
       totm' = proxy totientFact (Proxy::Proxy m')
   output :: t m r <- divGPow $ scalarPow $ fromIntegral $ mhat * totm' `div` totm
   input :: t m' r <- divGPow $ scalarPow $ fromIntegral mhat'
-  return $ (twacePowDec input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))
+  return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 -- twace mhat'/g' = mhat*totm'/totm/g (Dec basis)
 prop_twace_invar1_dec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool
@@ -288,7 +292,7 @@
       totm' = proxy totientFact (Proxy::Proxy m')
   output :: t m r <- divGDec $ lInv $ scalarPow $ fromIntegral $ mhat * totm' `div` totm
   input :: t m' r <- divGDec $ lInv $ scalarPow $ fromIntegral mhat'
-  return $ (twacePowDec input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))
+  return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 -- twace mhat'/g' = mhat*totm'/totm/g (CRT basis)
 prop_twace_invar1_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool
@@ -304,14 +308,14 @@
   twaceCRT' <- twaceCRT
   let output :: t m r = divGCRT1 $ scalarCRT1 $ fromIntegral $ mhat * totm' `div` totm
       input :: t m' r = divGCRT2 $ scalarCRT2 $ fromIntegral mhat'
-  return $ (twaceCRT' input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))
+  return $ (twaceCRT' input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 -- twace preserves scalars in Pow/Dec basis
 prop_twace_invar2_powdec :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool
 prop_twace_invar2_powdec _ _ = 
   let output = scalarPow $ one :: t m r
       input = scalarPow $ one :: t m' r
-  in (twacePowDec input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))
+  in (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 -- twace preserves scalars in Pow/Dec basis
 prop_twace_invar2_crt :: forall t m m' r . (TMM'RCtx t m m' r) => Proxy m' -> Proxy (t m r) -> Bool
@@ -320,7 +324,7 @@
   scalarCRT2 <- scalarCRT
   let input = scalarCRT1 one :: t m' r
       output = scalarCRT2 one :: t m r
-  return $ (twacePowDec input) == output \\ proxy entailFullT (Proxy::Proxy (t m r))
+  return $ (twacePowDec input) == output \\ proxy entailEqT (Proxy::Proxy (t m r))
 
 type TMM'RWrapCtx t m m' r = (TMM'RCtx t m m' r, Show (t m' r), Show (t m r), Arbitrary (t m' r), Arbitrary (t m r))