diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,33 @@
 Changelog
 =========
 
+Version 0.1.2.0
+---------------
+
+*October 14, 2018*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.2.0>
+
+*   New `:.:` for universe composition, with `Elem` and `Universe` instances,
+    and associated functions for working with them alongside `Any`, `All`.
+*   Many of the `Elem` instances and indices in *Data.Type.Universe* have had
+    their name changed to be more consistent with their role as indices.
+    `IsJust` is now `IJust`, `IsRight` is `IRight`, `Snd` is `ISnd`.
+*   Convenience predicates for alternate universes, such as `IsJust`, `IsLeft`,
+    `IsNothing`, etc.
+*   `NotAll` quantifier added alongside `None`.
+*   Many new implications added to *Data.Type.Predicate.Quantification*,
+    converting not-any and all-not, etc.
+*   `NotFound p` added as a convenience predicate synonym for `Not (Found p)`.
+*   Some implications showing the equivalence between `Found (InP f)` and
+    `NotNull f` added to *Data.Type.Predicate.Param*.
+*   Many new deduction rules added to *Data.Type.Predicate.Auto*.  Please see
+    module documentation for a detailed list of new rules and classes in this
+    version.
+*   Convenient combinators for dealing with `Refuted` and `Decision` added to
+    *Data.Type.Predicate*: `elimDisproof` and `mapRefuted.
+
+
 Version 0.1.1.0
 ---------------
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -7,6 +7,7 @@
 This library provides combinators and typeclasses for working and manipulating
 type-level predicates in Haskell, which are represented as matchable type-level
 functions `k ~> Type` from the *singletons* library.  See *Data.Type.Predicate*
-for a good starting point.
+for a good starting point, and the documentation for `Predicate` on how to
+define predicates.
 
 [decidable]: http://hackage.haskell.org/package/decidable
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -2,12 +2,16 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 24f4181ba9122110e3a7d932fd7820c169b392a5cdbc76825cd8f60f5410f0e3
+-- hash: 81cda78c02736265f023817475cdcf593f3a1cd1d8601f09bf92e4719d064fc1
 
 name:           decidable
-version:        0.1.1.0
+version:        0.1.2.0
 synopsis:       Combinators for manipulating dependently-typed predicates.
-description:    Please see the README on GitHub at <https://github.com/mstksg/decidable#readme>
+description:    This library provides combinators and typeclasses for working and manipulating
+                type-level predicates in Haskell, which are represented as matchable type-level
+                functions @k ~> Type@ from the @singletons@ library.  See "Data.Type.Predicate"
+                for a good starting point, and the documentation for 'Predicate' on how to
+                define predicates.
 category:       Dependent Types
 homepage:       https://github.com/mstksg/decidable#readme
 bug-reports:    https://github.com/mstksg/decidable/issues
diff --git a/src/Data/Type/Predicate.hs b/src/Data/Type/Predicate.hs
--- a/src/Data/Type/Predicate.hs
+++ b/src/Data/Type/Predicate.hs
@@ -1,20 +1,15 @@
-{-# LANGUAGE AllowAmbiguousTypes    #-}
-{-# LANGUAGE ConstraintKinds        #-}
-{-# LANGUAGE DefaultSignatures      #-}
-{-# LANGUAGE EmptyCase              #-}
-{-# LANGUAGE FlexibleContexts       #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE GADTs                  #-}
-{-# LANGUAGE LambdaCase             #-}
-{-# LANGUAGE MultiParamTypeClasses  #-}
-{-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE ScopedTypeVariables    #-}
-{-# LANGUAGE TemplateHaskell        #-}
-{-# LANGUAGE TypeApplications       #-}
-{-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE TypeInType             #-}
-{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds     #-}
+{-# LANGUAGE DefaultSignatures   #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeInType          #-}
+{-# LANGUAGE TypeOperators       #-}
 
 -- |
 -- Module      : Data.Type.Predicate
@@ -50,7 +45,9 @@
   -- * Manipulate Decisions
   , Decision(..)
   , flipDecision, mapDecision
+  , elimDisproof
   , forgetDisproof, forgetProof, isProved, isDisproved
+  , mapRefuted
   ) where
 
 import           Data.Kind
@@ -320,11 +317,11 @@
 instance Provable Evident where
     prove = id
 
-instance (Decidable f, SingI g) => Decidable (f .@#@$$$ g) where
-    decide = decide @f . ((sing :: Sing g) @@)
+instance (Decidable p, SingI f) => Decidable (PMap f p) where
+    decide = decide @p . ((sing :: Sing f) @@)
 
-instance (Provable f, SingI g) => Provable (f .@#@$$$ g) where
-    prove = prove @f . ((sing :: Sing g) @@)
+instance (Provable p, SingI f) => Provable (PMap f p) where
+    prove = prove @p . ((sing :: Sing f) @@)
 
 -- | Compose two implications.
 compImpl
@@ -355,7 +352,7 @@
 -- of not-@a@.
 --
 -- Note that this is not reversible in general in Haskell.  See
--- 'doubleNegation' for a situation where it is.
+-- 'Data.Type.Predicate.Logic.doubleNegation' for a situation where it is.
 --
 -- @since 0.1.1.0
 flipDecision
@@ -372,8 +369,8 @@
     -> Decision a
     -> Decision b
 mapDecision f g = \case
-    Proved    p -> Proved $ f p
-    Disproved v -> Disproved $ v . g
+    Proved    p -> Proved    $ f p
+    Disproved v -> Disproved $ mapRefuted g v
 
 -- | Converts a 'Decision' to a 'Maybe'.  Drop the witness of disproof of
 -- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if
@@ -407,3 +404,25 @@
 -- @since 0.1.1.0
 isDisproved :: Decision a -> Bool
 isDisproved = isNothing . forgetDisproof
+
+-- | Helper function for a common pattern of eliminating the disproved
+-- branch of 'Decision' to certaintify the proof.
+--
+-- @since 0.1.2.0
+elimDisproof
+    :: Decision a
+    -> Refuted (Refuted a)
+    -> a
+elimDisproof = \case
+    Proved    p -> const p
+    Disproved v -> absurd . ($ v)
+
+-- | Change the target of a 'Refuted' with a contravariant mapping
+-- function.
+--
+-- @since 0.1.2.0
+mapRefuted
+    :: (a -> b)
+    -> Refuted b
+    -> Refuted a
+mapRefuted = flip (.)
diff --git a/src/Data/Type/Predicate/Auto.hs b/src/Data/Type/Predicate/Auto.hs
--- a/src/Data/Type/Predicate/Auto.hs
+++ b/src/Data/Type/Predicate/Auto.hs
@@ -1,17 +1,17 @@
 {-# LANGUAGE AllowAmbiguousTypes   #-}
-{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE EmptyCase             #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeInType            #-}
 {-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
+{-# LANGUAGE UndecidableInstances  #-}
 
 -- |
 -- Module      : Data.Type.Predicate.Auto
@@ -27,16 +27,25 @@
 --
 -- @since 0.1.1.0
 module Data.Type.Predicate.Auto (
+  -- * Automatically generate witnesses at compile-time
     Auto(..)
-  , AutoElem(..)
+  , AutoNot, autoNot
   , AutoProvable
+  -- ** Helper classes
+  , AutoElem(..)
+  , AutoAll(..)
+  -- * Auto with help
+  , autoAny, autoNotAll
   ) where
 
-import           Data.List.NonEmpty        (NonEmpty(..))
+import           Data.List.NonEmpty                 (NonEmpty(..))
 import           Data.Singletons
+import           Data.Singletons.Sigma
 import           Data.Type.Equality
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
+import           Data.Type.Predicate.Param
+import           Data.Type.Predicate.Quantification
 import           Data.Type.Universe
 
 -- | Automatically generate a witness for predicate @p@ applied to input
@@ -48,6 +57,21 @@
 --
 -- Very close in nature to the @Known@ typeclass in the /type-combinators/
 -- library.
+--
+-- Admittedly this interface is a bit clunky and ad-hoc; at this point you
+-- can just try writing 'auto' in your code and praying that it works.  You
+-- always have the option, of course, to just manually write proofs.  If
+-- you have any inference rules to suggest, feel free to submit a PR!
+--
+-- An important limitation of 'Auto' is the Haskell type system prevents
+-- "either-or" constraints; this could potentially be implemented using
+-- compiler plugins.
+--
+-- One consequence of this is that it is impossible to automatically derive
+-- @'Any' f p@ and @'Not' ('All' f p)@.
+--
+-- For these, the compiler needs help; you can use 'autoAny' and
+-- 'autoNotAll' for these situations.
 class Auto (p :: Predicate k) (a :: k) where
     -- | Have the compiler generate a witness for @p \@\@ a@.
     --
@@ -61,6 +85,10 @@
 instance SingI a => Auto Evident a where
     auto = sing
 
+-- | @since 0.1.2.0
+instance SingI a => Auto (Not Impossible) a where
+    auto = ($ sing)
+
 instance Auto (EqualTo a) a where
     auto = Refl
 
@@ -91,7 +119,7 @@
     auto = prove @p @a sing
 
 -- | Typeclass representing 'Elem's pointing to an @a :: k@ that can be
--- generated automatically from type-level collection @as :: f k@.  
+-- generated automatically from type-level collection @as :: f k@.
 --
 -- If GHC knows both the type-level collection and the element you want to
 -- find at compile-time, this instance should allow it to find it.
@@ -123,10 +151,10 @@
     autoElem = IS autoElem
 
 instance AutoElem Maybe ('Just a) a where
-    autoElem = IsJust
+    autoElem = IJust
 
 instance AutoElem (Either j) ('Right a) a where
-    autoElem = IsRight
+    autoElem = IRight
 
 instance AutoElem NonEmpty (a ':| as) a where
     autoElem = NEHead
@@ -134,6 +162,149 @@
 instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where
     autoElem = NETail autoElem
 
+-- | @since 0.1.2.0
+instance AutoElem ((,) j) '(w, a) a where
+    autoElem = ISnd
+
+-- TODO: ???
+-- instance AutoElem (f :.: g) p ('Comp ass) where
+
 instance AutoElem f as a => Auto (In f as) a where
     auto = autoElem @f @as @a
 
+-- | Helper class for deriving 'Auto' instances for 'All' predicates; each
+-- 'Universe' instance is expected to implement these if possible, to get
+-- free 'Auto' instaces for their 'All' predicates.
+--
+-- Also helps for 'Not' 'Any' predicates and 'Not' 'Found' 'AnyMatch'
+-- predicates.
+--
+-- @since 0.1.2.0
+class AutoAll f (p :: Predicate k) (as :: f k) where
+    -- | Generate an 'All' for a given predicate over all items in @as@.
+    autoAll :: All f p @@ as
+
+instance AutoAll [] p '[] where
+    autoAll = WitAll $ \case {}
+
+instance (Auto p a, AutoAll [] p as) => AutoAll [] p (a ': as) where
+    autoAll = WitAll $ \case
+        IZ   -> auto @_ @p @a
+        IS i -> runWitAll (autoAll @[] @p @as) i
+
+instance AutoAll Maybe p 'Nothing where
+    autoAll = WitAll $ \case {}
+
+instance Auto p a => AutoAll Maybe p ('Just a) where
+    autoAll = WitAll $ \case IJust -> auto @_ @p @a
+
+instance AutoAll (Either j) p ('Left e) where
+    autoAll = WitAll $ \case {}
+
+instance Auto p a => AutoAll (Either j) p ('Right a) where
+    autoAll = WitAll $ \case IRight -> auto @_ @p @a
+
+instance (Auto p a, AutoAll [] p as) => AutoAll NonEmpty p (a ':| as) where
+    autoAll = WitAll $ \case
+        NEHead   -> auto @_ @p @a
+        NETail i -> runWitAll (autoAll @[] @p @as) i
+
+instance AutoAll f (All g p) ass => AutoAll (f :.: g) p ('Comp ass) where
+    autoAll = WitAll $ \(i :? j) ->
+      runWitAll (runWitAll (autoAll @f @(All g p) @ass) i) j
+
+instance Auto p a => AutoAll ((,) j) p '(w, a) where
+    autoAll = WitAll $ \case ISnd -> auto @_ @p @a
+
+-- | @since 0.1.2.0
+instance AutoAll f p as => Auto (All f p) as where
+    auto = autoAll @f @p @as
+
+-- | @since 0.1.2.0
+instance SingI a => Auto (NotNull []) (a ': as) where
+    auto = WitAny IZ sing
+
+-- | @since 0.1.2.0
+instance SingI a => Auto IsJust ('Just a) where
+    auto = WitAny IJust sing
+
+-- | @since 0.1.2.0
+instance SingI a => Auto IsRight ('Right a) where
+    auto = WitAny IRight sing
+
+-- | @since 0.1.2.0
+instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where
+    auto = WitAny NEHead sing
+
+-- | @since 0.1.2.0
+instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
+    auto = WitAny ISnd sing
+
+-- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to not be
+-- true at compiletime.
+--
+-- @since 0.1.2.0
+type AutoNot (p :: Predicate k) = Auto (Not p)
+
+-- | Disprove @p \@\@ a@ at compiletime.
+--
+-- @
+-- autoNot @_ @p @a :: Not p @@ a
+-- @
+--
+-- @since 0.1.2.0
+autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a
+autoNot = auto @k @(Not p) @a
+
+-- | @since 0.1.2.0
+instance Auto (Found p) (f @@ a) => Auto (Found (PPMap f p)) a where
+    auto = case auto @_ @(Found p) @(f @@ a) of
+        i :&: p -> i :&: p
+
+-- | @since 0.1.2.0
+instance Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p)) a where
+    auto = mapRefuted (\(i :&: p) -> i :&: p)
+         $ autoNot @_ @(Found p) @(f @@ a)
+
+-- | @since 0.1.2.0
+instance Auto p (f @@ a) => Auto (PMap f p) a where
+    auto = auto @_ @p @(f @@ a)
+
+-- | @since 0.1.2.0
+instance AutoNot p (f @@ a) => Auto (Not (PMap f p)) a where
+    auto = autoNot @_ @p @(f @@ a)
+
+-- | Helper function to generate an @'Any' f p@ if you can pick out
+-- a specific @a@ in @as@ where the predicate is provable at compile-time.
+--
+-- This is used to get around a fundamental limitation of 'Auto' as
+-- a Haskell typeclass.
+--
+-- @since 0.1.2.0
+autoAny
+    :: forall f p as a. Auto p a
+    => Elem f as a
+    -> Any f p @@ as
+autoAny i = WitAny i (auto @_ @p @a)
+
+-- | @since 0.1.2.0
+instance (SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p)) as where
+    auto = allNotNone sing $ autoAll @f @(Not p) @as
+
+-- | Helper function to generate a @'Not' ('All' f p)@ if you can pick out
+-- a specific @a@ in @as@ where the predicate is disprovable at compile-time.
+--
+-- This is used to get around a fundamental limitation of 'Auto' as
+-- a Haskell typeclass.
+--
+-- @since 0.1.2.0
+autoNotAll
+    :: forall p f as a. (AutoNot p a, SingI as)
+    => Elem f as a
+    -> Not (All f p) @@ as
+autoNotAll = anyNotNotAll sing . autoAny
+
+-- | @since 0.1.2.0
+instance (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p))) as where
+    auto = mapRefuted (\(s :&: WitAny i p) -> WitAny i (s :&: p))
+         $ auto @_ @(Not (Any f (Found p))) @as
diff --git a/src/Data/Type/Predicate/Logic.hs b/src/Data/Type/Predicate/Logic.hs
--- a/src/Data/Type/Predicate/Logic.hs
+++ b/src/Data/Type/Predicate/Logic.hs
@@ -1,11 +1,11 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds     #-}
-{-# LANGUAGE EmptyCase           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE FlexibleInstances   #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE TypeApplications    #-}
 {-# LANGUAGE TypeFamilies        #-}
 {-# LANGUAGE TypeInType          #-}
@@ -63,9 +63,7 @@
     -> Decision (q @@ a)
     -> Decision ((p &&& q) @@ a)
 decideAnd = \case
-    Proved p    -> \case
-      Proved q    -> Proved (p, q)
-      Disproved v -> Disproved $ \(_, q) -> v q
+    Proved p    -> mapDecision (p,) snd
     Disproved v -> \_ -> Disproved $ \(p, _) -> v p
 
 -- | @p '|||' q@ is a predicate that either @p@ and @q@ are true.
@@ -84,11 +82,7 @@
     -> Decision ((p ||| q) @@ a)
 decideOr = \case
     Proved p    -> \_ -> Proved $ Left p
-    Disproved v -> \case
-      Proved q    -> Proved $ Right q
-      Disproved w -> Disproved $ \case
-        Left p  -> v p
-        Right q -> w q
+    Disproved v -> mapDecision Right (either (absurd . v) id)
 
 -- | Left-biased "or".  In proofs, prioritize a proof of the left side over
 -- a proof of the right side.
@@ -227,15 +221,13 @@
     :: forall p q. Decidable q
     => (Not q --> Not p)
     -> (p --> q)
-contrapositive' f x p = case decide @q x of
-    Proved     q -> q
-    Disproved vq -> absurd $ f x vq p
+contrapositive' f x p = elimDisproof (decide @q x) $ \vQ ->
+    f x vQ p
 
 -- | Logical double negation.  Only possible if @p@ is 'Decidable'.
 doubleNegation :: forall p. Decidable p => Not (Not p) --> p
-doubleNegation x vvp = case decide @p x of
-    Proved    p  -> p
-    Disproved vp -> absurd $ vvp vp
+doubleNegation x vvP = elimDisproof (decide @p x) $ \vP ->
+    vvP vP
 
 -- | If @p '&&&' q@ is true, then so is @p@.
 projAndFst :: (p &&& q) --> p
diff --git a/src/Data/Type/Predicate/Param.hs b/src/Data/Type/Predicate/Param.hs
--- a/src/Data/Type/Predicate/Param.hs
+++ b/src/Data/Type/Predicate/Param.hs
@@ -1,6 +1,4 @@
 {-# LANGUAGE ConstraintKinds      #-}
-{-# LANGUAGE DefaultSignatures    #-}
-{-# LANGUAGE EmptyCase            #-}
 {-# LANGUAGE FlexibleContexts     #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE LambdaCase           #-}
@@ -9,7 +7,6 @@
 {-# LANGUAGE TypeFamilies         #-}
 {-# LANGUAGE TypeInType           #-}
 {-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- |
@@ -29,9 +26,10 @@
     ParamPred
   , FlipPP, ConstPP, PPMap, InP, AnyMatch
   -- * Deciding and Proving
-  , Found
+  , Found, NotFound
   , Selectable, select
   , Searchable, search
+  , inPNotNull, notNullInP
   ) where
 
 import           Data.Singletons
@@ -54,17 +52,38 @@
 --
 -- For some context, an instance of @'Provable' ('Found' P)@, where @P ::
 -- 'ParamPred' k v@, means that for any input @x :: k@, we can always find
--- a @y :: v@ such that we have @P x @@ y@.
+-- a @y :: v@ such that we have @P x \@\@ y@.
 --
 -- In the language of quantifiers, it means that forall @x :: k@, there
--- exists a @y :: v@ such that @P x @@ y@.
+-- exists a @y :: v@ such that @P x \@\@ y@.
 --
 -- For an instance of @'Decidable' ('Found' P)@, it means that for all @x
 -- :: k@, we can prove or disprove the fact that there exists a @y :: v@
--- such that @P x @@ y@.
+-- such that @P x \@\@ y@.
 data Found :: ParamPred k v -> Predicate k
 type instance Apply (Found (p :: ParamPred k v)) a = Σ v (p a)
 
+-- | Convert a parameterized predicate into a predicate on the parameter.
+--
+-- A @'Found' p@ is a predicate on @p :: 'ParamPred' k v@ that tests a @k@
+-- for the fact that there /cannot exist/ a @v@ where @'ParamPred' k v@ is
+-- satisfied.  That is, @'NotFound' P \@\@ x@ is satisfied if no @y :: v@
+-- can exist where @P x \@\@ y@ is satisfied.
+--
+-- For some context, an instance of @'Provable' ('NotFound' P)@, where @P
+-- :: 'ParamPred' k v@, means that for any input @x :: k@, we can always
+-- reject any @y :: v@ that claims to satisfy @P x \@\@ y@.
+--
+-- In the language of quantifiers, it means that forall @x :: k@, there
+-- does not exist a @y :: v@ such that @P x \@\@ y@.
+--
+-- For an instance of @'Decidable' ('Found' P)@, it means that for all @x
+-- :: k@, we can prove or disprove the fact that there does not exist a @y
+-- :: v@ such that @P x \@\@ y@.
+--
+-- @since 0.1.2.0
+type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k)
+
 -- | Flip the arguments of a 'ParamPred'.
 data FlipPP :: ParamPred v k -> ParamPred k v
 type instance Apply (FlipPP p x) y = p y @@ x
@@ -131,6 +150,18 @@
 -- Essentially 'NotNull'.
 type InP f = (ElemSym1 f :: ParamPred (f k) k)
 
+-- | @'NotNull' f@ is basically @'Found' ('InP' f)@.
+--
+-- @since 0.1.2.0
+notNullInP :: NotNull f --> Found (InP f)
+notNullInP _ (WitAny i s) = s :&: i
+
+-- | @'NotNull' f@ is basically @'Found' ('InP' f)@.
+--
+-- @since 0.1.2.0
+inPNotNull :: Found (InP f) --> NotNull f
+inPNotNull _ (s :&: i) = WitAny i s
+
 instance Universe f => Decidable (Found (InP f)) where
     decide = mapDecision (\case WitAny i s -> s :&: i    )
                          (\case s :&: i     -> WitAny i s)
@@ -138,11 +169,11 @@
 
 instance Decidable (NotNull f ==> Found (InP f))
 instance Provable (NotNull f ==> Found (InP f)) where
-    prove _ (WitAny i s) = s :&: i
+    prove = notNullInP
 
 instance Decidable (Found (InP f) ==> NotNull f)
 instance Provable (Found (InP f) ==> NotNull f) where
-    prove _ (s :&: i) = WitAny i s
+    prove = inPNotNull
 
 -- | @'AnyMatch' f@ takes a parmaeterized predicate on @k@ (testing for
 -- a @v@) and turns it into a parameterized predicate on @f k@ (testing for
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
--- a/src/Data/Type/Predicate/Quantification.hs
+++ b/src/Data/Type/Predicate/Quantification.hs
@@ -1,18 +1,10 @@
-{-# LANGUAGE AllowAmbiguousTypes   #-}
-{-# LANGUAGE EmptyCase             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE LambdaCase            #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeInType          #-}
+{-# LANGUAGE TypeOperators       #-}
 
 -- |
 -- Module      : Data.Type.Predicate.Quantification
@@ -28,18 +20,27 @@
 --
 module Data.Type.Predicate.Quantification (
   -- * Any
-    Any, WitAny(..), None
+    Any, WitAny(..), anyImpossible
   -- ** Decision
   , decideAny, idecideAny, decideNone, idecideNone
+  -- ** Negation
+  , None, allNotNone, noneAllNot
   -- ** Entailment
   , entailAny, ientailAny, entailAnyF, ientailAnyF
+  -- ** Composition
+  , allComp, compAll
   -- * All
   , All, WitAll(..)
   -- ** Decision
   , decideAll, idecideAll
+  -- ** Negation
+  , NotAll
+  , anyNotNotAll, notAllAnyNot
   -- ** Entailment
   , entailAll, ientailAll, entailAllF, ientailAllF
   , decideEntailAll, idecideEntailAll
+  -- ** Composition
+  , anyComp, compAny
   ) where
 
 import           Data.Kind
@@ -157,3 +158,46 @@
     => p -?> q
     -> All f p -?> All f q
 decideEntailAll = dmap @(All f)
+
+-- | It is impossible for any value in a collection to be 'Impossible'.
+--
+-- @since 0.1.2.0
+anyImpossible :: Universe f => Any f Impossible --> Impossible
+anyImpossible _ (WitAny i p) = p . index i
+
+-- | If any @a@ in @as@ does not satisfy @p@, then not all @a@ in @as@
+-- satisfy @p@.
+--
+-- @since 0.1.2.0
+anyNotNotAll :: Any f (Not p) --> NotAll f p
+anyNotNotAll _ (WitAny i v) a = v $ runWitAll a i
+
+-- | If not all @a@ in @as@ satisfy @p@, then there must be at least one
+-- @a@ in @as@ that does not satisfy @p@.  Requires @'Decidable' p@ in
+-- order to locate that specific @a@.
+--
+-- @since 0.1.2.0
+notAllAnyNot
+    :: forall f p. (Universe f, Decidable p)
+    => NotAll f p --> Any f (Not p)
+notAllAnyNot xs vAll = elimDisproof (decide @(Any f (Not p)) xs) $ \vAny ->
+    vAll $ WitAll $ \i ->
+      elimDisproof (decide @p (index i xs)) $ \vP ->
+        vAny $ WitAny i vP
+
+-- | If @p@ is false for all @a@ in @as@, then no @a@ in @as@ satisfies
+-- @p@.
+--
+-- @since 0.1.2.0
+allNotNone :: All f (Not p) --> None f p
+allNotNone _ a (WitAny i v) = runWitAll a i v
+
+-- | If no @a@ in @as@ satisfies @p@, then @p@ is false for all @a@ in
+-- @as@.  Requires @'Decidable' p@ to interrogate the input disproof.
+--
+-- @since 0.1.2.0
+noneAllNot
+    :: forall f p. (Universe f, Decidable p)
+    => None f p --> All f (Not p)
+noneAllNot xs vAny = elimDisproof (decide @(All f (Not p)) xs) $ \vAll ->
+    vAll $ WitAll $ \i p -> vAny $ WitAny i p
diff --git a/src/Data/Type/Universe.hs b/src/Data/Type/Universe.hs
--- a/src/Data/Type/Universe.hs
+++ b/src/Data/Type/Universe.hs
@@ -1,19 +1,20 @@
-{-# LANGUAGE EmptyCase             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE InstanceSigs          #-}
-{-# LANGUAGE LambdaCase            #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE StandaloneDeriving    #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE DeriveFunctor        #-}
+{-# LANGUAGE DeriveGeneric        #-}
+{-# LANGUAGE DeriveTraversable    #-}
+{-# LANGUAGE EmptyCase            #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE InstanceSigs         #-}
+{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeInType           #-}
+{-# LANGUAGE TypeOperators        #-}
 
 -- |
 -- Module      : Data.Type.Universe
@@ -31,27 +32,35 @@
   -- * Universe
     Elem, In, Universe(..)
   -- ** Instances
-  , Index(..), IsJust(..), IsRight(..), NEIndex(..), Snd(..)
+  , Index(..), IJust(..), IRight(..), NEIndex(..), ISnd(..)
+  , CompElem(..)
   -- ** Predicates
-  , All, WitAll(..)
+  , All, WitAll(..), NotAll
   , Any, WitAny(..), None
   , Null, NotNull
+  -- *** Specialized
+  , IsJust, IsNothing, IsRight, IsLeft
   -- * Decisions and manipulations
   , decideAny, decideAll, genAllA, genAll, igenAll
   , foldMapUni, ifoldMapUni, index, pickElem
+  -- * Universe Composition
+  , (:.:)(..), Sing(SComp), sGetComp, GetComp
+  , allComp, compAll, anyComp, compAny
   -- * Defunctionalization symbols
-  , ElemSym0, ElemSym1, ElemSym2
+  , ElemSym0, ElemSym1, ElemSym2, GetCompSym0, GetCompSym1
   ) where
 
-import           Data.Type.Predicate.Logic
 import           Control.Applicative
 import           Data.Functor.Identity
 import           Data.Kind
 import           Data.List.NonEmpty                    (NonEmpty(..))
 import           Data.Singletons
 import           Data.Singletons.Decide
-import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Snd, Null, Not)
+import           Data.Singletons.Prelude hiding        (Elem, ElemSym0, ElemSym1, ElemSym2, Any, All, Null, Not)
 import           Data.Type.Predicate
+import           Data.Type.Predicate.Logic
+import           Data.Typeable                         (Typeable)
+import           GHC.Generics                          (Generic)
 import           Prelude hiding                        (any, all)
 import qualified Data.Singletons.Prelude.List.NonEmpty as NE
 
@@ -152,6 +161,10 @@
 -- satisfies predicate @p@.
 type None f p = (Not (Any f p) :: Predicate (f k))
 
+-- | A @'NotAll' f p@ is a predicate on a collection @as@ that at least one
+-- @a@ in @as@ does not satisfy predicate @p@.
+type NotAll f p = (Not (All f p) :: Predicate (f k))
+
 -- | Lifts a predicate @p@ on an individual @a@ into a predicate that on
 -- a collection @as@ that is true if and only if /any/ item in @as@
 -- satisfies the original predicate.
@@ -310,61 +323,81 @@
 
 -- | Witness an item in a type-level 'Maybe' by proving the 'Maybe' is
 -- 'Just'.
-data IsJust :: Maybe k -> k -> Type where
-    IsJust :: IsJust ('Just a) a
+data IJust :: Maybe k -> k -> Type where
+    IJust :: IJust ('Just a) a
 
-deriving instance Show (IsJust as a)
-instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IsJust as)) where
+deriving instance Show (IJust as a)
+instance (SingI (as :: Maybe k), SDecide k) => Decidable (TyPred (IJust as)) where
     decide x = withSingI x $ pickElem
 
-type instance Elem Maybe = IsJust
+type instance Elem Maybe = IJust
 
+-- | Test that a 'Maybe' is 'Just'.
+--
+-- @since 0.1.2.0
+type IsJust    = (NotNull Maybe :: Predicate (Maybe k))
+
+-- | Test that a 'Maybe' is 'Nothing'.
+--
+-- @since 0.1.2.0
+type IsNothing = (Null    Maybe :: Predicate (Maybe k))
+
 instance Universe Maybe where
     idecideAny f = \case
       SNothing -> Disproved $ \case WitAny i _ -> case i of {}
-      SJust x  -> case f IsJust x of
-        Proved p    -> Proved $ WitAny IsJust p
+      SJust x  -> case f IJust x of
+        Proved p    -> Proved $ WitAny IJust p
         Disproved v -> Disproved $ \case
-          WitAny IsJust p -> v p
+          WitAny IJust p -> v p
 
     idecideAll f = \case
       SNothing -> Proved $ WitAll $ \case {}
-      SJust x  -> case f IsJust x of
-        Proved p    -> Proved $ WitAll $ \case IsJust -> p
-        Disproved v -> Disproved $ \a -> v $ runWitAll a IsJust
+      SJust x  -> case f IJust x of
+        Proved p    -> Proved $ WitAll $ \case IJust -> p
+        Disproved v -> Disproved $ \a -> v $ runWitAll a IJust
 
     igenAllA f = \case
       SNothing -> pure $ WitAll $ \case {}
-      SJust x  -> (\p -> WitAll $ \case IsJust -> p) <$> f IsJust x
+      SJust x  -> (\p -> WitAll $ \case IJust -> p) <$> f IJust x
 
 -- | Witness an item in a type-level @'Either' j@ by proving the 'Either'
 -- is 'Right'.
-data IsRight :: Either j k -> k -> Type where
-    IsRight :: IsRight ('Right a) a
+data IRight :: Either j k -> k -> Type where
+    IRight :: IRight ('Right a) a
 
-deriving instance Show (IsRight as a)
-instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IsRight as)) where
+deriving instance Show (IRight as a)
+instance (SingI (as :: Either j k), SDecide k) => Decidable (TyPred (IRight as)) where
     decide x = withSingI x $ pickElem
 
-type instance Elem (Either j) = IsRight
+type instance Elem (Either j) = IRight
 
+-- | Test that an 'Either' is 'Right'
+--
+-- @since 0.1.2.0
+type IsRight = (NotNull (Either j) :: Predicate (Either j k))
+
+-- | Test that an 'Either' is 'Left'
+--
+-- @since 0.1.2.0
+type IsLeft  = (Null    (Either j) :: Predicate (Either j k))
+
 instance Universe (Either j) where
     idecideAny f = \case
       SLeft  _ -> Disproved $ \case WitAny i _ -> case i of {}
-      SRight x -> case f IsRight x of
-        Proved p    -> Proved $ WitAny IsRight p
+      SRight x -> case f IRight x of
+        Proved p    -> Proved $ WitAny IRight p
         Disproved v -> Disproved $ \case
-          WitAny IsRight p -> v p
+          WitAny IRight p -> v p
 
     idecideAll f = \case
       SLeft  _ -> Proved $ WitAll $ \case {}
-      SRight x -> case f IsRight x of
-        Proved p    -> Proved $ WitAll $ \case IsRight -> p
-        Disproved v -> Disproved $ \a -> v $ runWitAll a IsRight
+      SRight x -> case f IRight x of
+        Proved p    -> Proved $ WitAll $ \case IRight -> p
+        Disproved v -> Disproved $ \a -> v $ runWitAll a IRight
 
     igenAllA f = \case
       SLeft  _ -> pure $ WitAll $ \case {}
-      SRight x -> (\p -> WitAll $ \case IsRight -> p) <$> f IsRight x
+      SRight x -> (\p -> WitAll $ \case IRight -> p) <$> f IRight x
 
 -- | Witness an item in a type-level 'NonEmpty' by either indicating that
 -- it is the "head", or by providing an index in the "tail".
@@ -419,22 +452,142 @@
           NETail i -> runWitAll ps i
 
 -- | Trivially witness an item in the second field of a type-level tuple.
-data Snd :: (j, k) -> k -> Type where
-    Snd :: Snd '(a, b) b
+data ISnd :: (j, k) -> k -> Type where
+    ISnd :: ISnd '(a, b) b
 
-deriving instance Show (Snd as a)
-instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (Snd as)) where
+deriving instance Show (ISnd as a)
+-- TODO: does this interfere with NonNull stuff?
+instance (SingI (as :: (j, k)), SDecide k) => Decidable (TyPred (ISnd as)) where
     decide x = withSingI x $ pickElem
 
-type instance Elem ((,) j) = Snd
+type instance Elem ((,) j) = ISnd
 
 instance Universe ((,) j) where
-    idecideAny f (STuple2 _ x) = case f Snd x of
-      Proved p    -> Proved $ WitAny Snd p
-      Disproved v -> Disproved $ \case WitAny Snd p -> v p
+    idecideAny f (STuple2 _ x) = case f ISnd x of
+      Proved p    -> Proved $ WitAny ISnd p
+      Disproved v -> Disproved $ \case WitAny ISnd p -> v p
 
-    idecideAll f (STuple2 _ x) = case f Snd x of
-      Proved p    -> Proved $ WitAll $ \case Snd -> p
-      Disproved v -> Disproved $ \a -> v $ runWitAll a Snd
+    idecideAll f (STuple2 _ x) = case f ISnd x of
+      Proved p    -> Proved $ WitAll $ \case ISnd -> p
+      Disproved v -> Disproved $ \a -> v $ runWitAll a ISnd
 
-    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case Snd -> p) <$> f Snd x
+    igenAllA f (STuple2 _ x) = (\p -> WitAll $ \case ISnd -> p) <$> f ISnd x
+
+-- | Compose two Functors.  Is the same as 'Data.Functor.Compose.Compose'
+-- and 'GHC.Generics.:.:', except with a singleton and meant to be used at
+-- the type level.  Will be redundant if either of the above gets brought
+-- into the singletons library.
+--
+-- Note that because this is a higher-kinded data constructor, there is no
+-- 'SingKind'  instance; if you need 'fromSing' and 'toSing', try going
+-- through 'Comp' and 'getComp' and 'SComp' and 'sGetComp'.
+--
+-- @since 0.1.2.0
+data (f :.: g) a = Comp { getComp :: f (g a) }
+    deriving (Show, Eq, Ord, Functor, Foldable, Typeable, Generic)
+deriving instance (Traversable f, Traversable g) => Traversable (f :.: g)
+
+data instance Sing (k :: (f :.: g) a) where
+    SComp :: Sing x -> Sing ('Comp x)
+
+-- | 'getComp' lifted to the type level
+--
+-- @since 0.1.2.0
+type family GetComp c where
+    GetComp ('Comp a) = a
+
+-- | Singletonized witness for 'GetComp'
+--
+-- @since 0.1.2.0
+sGetComp :: Sing a -> Sing (GetComp a)
+sGetComp (SComp x) = x
+ 
+instance SingI ass => SingI ('Comp ass) where
+    sing = SComp sing
+
+data GetCompSym0 :: (f :.: g) k ~> f (g k)
+type instance Apply GetCompSym0 ('Comp ass) = ass
+type GetCompSym1 a = GetComp a
+
+-- instance forall f g a f' g' a'. (SingKind (f (g a)), Demote (f (g a)) ~ f' (g' a')) => SingKind ((f :.: g) a) where
+--     type Demote ((f :.: g) a) = (:.:) f' g' a'
+
+-- | A pair of indices allows you to index into a nested structure.
+--
+-- @since 0.1.2.0
+data CompElem :: (f :.: g) k -> k -> Type where
+    (:?) :: Elem f ass as
+         -> Elem g as  a
+         -> CompElem ('Comp ass) a
+
+-- deriving instance ((forall as. Show (Elem f ass as)), (forall as. Show (Elem g as a)))
+--     => Show (CompElem ('Comp ass :: (f :.: g) k) a)
+
+type instance Elem (f :.: g) = CompElem
+
+instance (Universe f, Universe g) => Universe (f :.: g) where
+    idecideAny
+        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
+        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
+        -> Sing ass
+        -> Decision (Any (f :.: g) p @@ ass)
+    idecideAny f (SComp xss)
+        = mapDecision anyComp compAny
+        . idecideAny @f @_ @(Any g p) go
+        $ xss
+      where
+        go  :: Elem f (GetComp ass) as
+            -> Sing as
+            -> Decision (Any g p @@ as)
+        go i = idecideAny $ \j -> f (i :? j)
+
+    idecideAll
+        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k). ()
+        => (forall a. Elem (f :.: g) ass a -> Sing a -> Decision (p @@ a))
+        -> Sing ass
+        -> Decision (All (f :.: g) p @@ ass)
+    idecideAll f (SComp xss)
+        = mapDecision allComp compAll
+        . idecideAll @f @_ @(All g p) go
+        $ xss
+      where
+        go  :: Elem f (GetComp ass) as
+            -> Sing as
+            -> Decision (All g p @@ as)
+        go i = idecideAll $ \j -> f (i :? j)
+
+    igenAllA
+        :: forall k (p :: k ~> Type) (ass :: (f :.: g) k) h. Applicative h
+        => (forall a. Elem (f :.: g) ass a -> Sing a -> h (p @@ a))
+        -> Sing ass
+        -> h (All (f :.: g) p @@ ass)
+    igenAllA f (SComp ass) = allComp <$> igenAllA @f @_ @(All g p) go ass
+      where
+        go  :: Elem f (GetComp ass) (as :: g k)
+            -> Sing as
+            -> h (All g p @@ as)
+        go i = igenAllA $ \j -> f (i :? j)
+
+-- | Turn a composition of 'Any' into an 'Any' of a composition.
+--
+-- @since 0.1.2.0
+anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
+anyComp (WitAny i (WitAny j p)) = WitAny (i :? j) p
+
+-- | Turn an 'Any' of a composition into a composition of 'Any'.
+--
+-- @since 0.1.2.0
+compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
+compAny (WitAny (i :? j) p) = WitAny i (WitAny j p)
+
+-- | Turn a composition of 'All' into an 'All' of a composition.
+--
+-- @since 0.1.2.0
+allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
+allComp a = WitAll $ \(i :? j) -> runWitAll (runWitAll a i) j
+
+-- | Turn an 'All' of a composition into a composition of 'All'.
+--
+-- @since 0.1.2.0
+compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
+compAll a = WitAll $ \i -> WitAll $ \j -> runWitAll a (i :? j)
diff --git a/src/Data/Type/Universe/Subset.hs b/src/Data/Type/Universe/Subset.hs
--- a/src/Data/Type/Universe/Subset.hs
+++ b/src/Data/Type/Universe/Subset.hs
@@ -1,18 +1,10 @@
-{-# LANGUAGE AllowAmbiguousTypes   #-}
-{-# LANGUAGE EmptyCase             #-}
-{-# LANGUAGE FlexibleContexts      #-}
-{-# LANGUAGE FlexibleInstances     #-}
-{-# LANGUAGE GADTs                 #-}
-{-# LANGUAGE LambdaCase            #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE RankNTypes            #-}
-{-# LANGUAGE ScopedTypeVariables   #-}
-{-# LANGUAGE TypeApplications      #-}
-{-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE TypeOperators         #-}
-{-# LANGUAGE TypeSynonymInstances  #-}
-{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE TypeInType          #-}
+{-# LANGUAGE TypeOperators       #-}
 
 -- |
 -- Module      : Data.Type.Universe.Subset