diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,22 @@
 Changelog
 =========
 
+Version 0.1.1.0
+---------------
+
+*October 12, 2018*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.1.0>
+
+*   `flipDecision`, `forgetDisproof`, `forgetProof`, `isProved`, and
+    `isDisproved` added to *Data.Type.Predicate* module.
+*   `ProvableTC`, `DeccidableTC`, `proveTC`, and `decideTC` helper functions
+    and constraints
+*   *Data.Type.Predicate.Auto* module, for generating witnesses at
+    compile-time.
+*   Instances for injection and projection out of `&&&` and `|||`, with some
+    tricks to prevent overlapping instance issues.
+
 Version 0.1.0.0
 ---------------
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,11 +1,12 @@
-# [decidable][]
+[decidable][]
+=============
 
 [![decidable on Hackage](https://img.shields.io/hackage/v/decidable.svg?maxAge=86400)](https://hackage.haskell.org/package/decidable)
 [![Build Status](https://travis-ci.org/mstksg/decidable.svg?branch=master)](https://travis-ci.org/mstksg/decidable)
-[decidable]: https://mstksg.github.io/decidable/
 
 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.
 
+[decidable]: http://hackage.haskell.org/package/decidable
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -2,10 +2,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: fa635fe6f55a295cab015d273dc723b843bac34ddd35415b9495c1c9306ba671
+-- hash: 24f4181ba9122110e3a7d932fd7820c169b392a5cdbc76825cd8f60f5410f0e3
 
 name:           decidable
-version:        0.1.0.0
+version:        0.1.1.0
 synopsis:       Combinators for manipulating dependently-typed predicates.
 description:    Please see the README on GitHub at <https://github.com/mstksg/decidable#readme>
 category:       Dependent Types
@@ -30,6 +30,7 @@
 library
   exposed-modules:
       Data.Type.Predicate
+      Data.Type.Predicate.Auto
       Data.Type.Predicate.Logic
       Data.Type.Predicate.Param
       Data.Type.Predicate.Quantification
@@ -39,7 +40,7 @@
       Paths_decidable
   hs-source-dirs:
       src
-  ghc-options: -Wall -Wredundant-constraints
+  ghc-options: -Wall -Wredundant-constraints -Wcompat
   build-depends:
       base >=4.11 && <5
     , singletons >=2.4
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
@@ -39,16 +39,22 @@
   , Prove, type (-->), type (-->#)
   , Provable(..)
   , Disprovable, disprove
+  , ProvableTC, proveTC
   , TFunctor(..)
   , compImpl
     -- * Decidable Predicates
   , Decide, type (-?>), type (-?>#)
   , Decidable(..)
+  , DecidableTC, decideTC
   , DFunctor(..)
-  , mapDecision
+  -- * Manipulate Decisions
+  , Decision(..)
+  , flipDecision, mapDecision
+  , forgetDisproof, forgetProof, isProved, isDisproved
   ) where
 
 import           Data.Kind
+import           Data.Maybe
 import           Data.Singletons
 import           Data.Singletons.Decide
 import           Data.Singletons.Prelude hiding (Not)
@@ -150,6 +156,9 @@
 
 -- | A @'Wit' p a@ is a value of type @p \@\@ a@ --- that is, it is a proof
 -- or witness that @p@ is satisfied for @a@.
+--
+-- It essentially turns a @k ~> 'Type'@ ("matchable" @'Predicate' k@) /back
+-- into/ a @k -> 'Type'@ predicate.
 newtype Wit p a = Wit { getWit :: p @@ a }
 
 -- | A decision function for predicate @p@.  See 'Decidable' for more
@@ -253,6 +262,47 @@
 disprove :: forall p. Disprovable p => Prove (Not p)
 disprove = prove @(Not p)
 
+-- | If @T :: k -> 'Type'@ is a type constructor, then @'DecidableTC' T@ is
+-- a constraint that @T@ is "decidable", in that you have a canonical
+-- function:
+--
+-- @
+-- decideTC :: Sing a -> 'Decision' (T a)
+-- @
+--
+-- Is essentially 'Decidable', except with /type constructors/ @k ->
+-- 'Type'@ instead of matchable type-level functions (that are @k ~>
+-- 'Type'@).
+--
+-- @since 0.1.1.0
+type DecidableTC p = Decidable (TyPred p)
+
+-- | The canonical deciding function for @'DecidableTC' t@.
+--
+-- @since 0.1.1.0
+decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
+decideTC = decide @(TyPred t)
+
+-- | If @T :: k -> 'Type'@ is a type constructor, then @'ProvableTC' T@ is
+-- a constraint that @T@ is "decidable", in that you have a canonical
+-- function:
+--
+-- @
+-- proveTC :: Sing a -> T a
+-- @
+--
+-- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@
+-- instead of matchable type-level functions (that are @k ~> 'Type'@).
+--
+-- @since 0.1.1.0
+type ProvableTC  p = Provable  (TyPred p)
+
+-- | The canonical proving function for @'DecidableTC' t@.
+--
+-- @since 0.1.1.0
+proveTC :: forall t a. ProvableTC t => Sing a -> t a
+proveTC = prove @(TyPred t)
+
 -- | Implicatons @p '-?>' q@ can be lifted "through" a 'DFunctor' into an
 -- @f p '-?>' f q@.
 class DFunctor f where
@@ -299,8 +349,20 @@
     :: forall p a. ()
     => Decision (p @@ a)
     -> Decision (Not p @@ a)
-decideNot = \case
-    Proved p    -> Disproved ($ p)
+decideNot = flipDecision
+
+-- | Flip the contents of a decision.  Turn a proof of @a@ into a disproof
+-- of not-@a@.
+--
+-- Note that this is not reversible in general in Haskell.  See
+-- 'doubleNegation' for a situation where it is.
+--
+-- @since 0.1.1.0
+flipDecision
+    :: Decision a
+    -> Decision (Refuted a)
+flipDecision = \case
+    Proved    p -> Disproved ($ p)
     Disproved v -> Proved v
 
 -- | Map over the value inside a 'Decision'.
@@ -312,3 +374,36 @@
 mapDecision f g = \case
     Proved    p -> Proved $ f p
     Disproved v -> Disproved $ v . g
+
+-- | Converts a 'Decision' to a 'Maybe'.  Drop the witness of disproof of
+-- @a@, returning 'Just' if 'Proved' (with the proof) and 'Nothing' if
+-- 'Disproved'.
+--
+-- @since 0.1.1.0
+forgetDisproof
+    :: Decision a
+    -> Maybe a
+forgetDisproof = \case
+    Proved    p -> Just p
+    Disproved _ -> Nothing
+
+-- | Drop the witness of proof of @a@, returning 'Nothing' if 'Proved' and
+-- 'Just' if 'Disproved' (with the disproof).
+--
+-- @since 0.1.1.0
+forgetProof
+    :: Decision a
+    -> Maybe (Refuted a)
+forgetProof = forgetDisproof . flipDecision
+
+-- | Boolean test if a 'Decision' is 'Proved'.
+--
+-- @since 0.1.1.0
+isProved :: Decision a -> Bool
+isProved = isJust . forgetDisproof
+
+-- | Boolean test if a 'Decision' is 'Disproved'.
+--
+-- @since 0.1.1.0
+isDisproved :: Decision a -> Bool
+isDisproved = isNothing . forgetDisproof
diff --git a/src/Data/Type/Predicate/Auto.hs b/src/Data/Type/Predicate/Auto.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Predicate/Auto.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
+
+-- |
+-- Module      : Data.Type.Predicate.Auto
+-- Copyright   : (c) Justin Le 2018
+-- License     : BSD3
+--
+-- Maintainer  : justin@jle.im
+-- Stability   : experimental
+-- Portability : non-portable
+--
+-- Useful utilities for situations where you know that a predicate @P@ is
+-- satisfied for a specific @a@ at compile-time.
+--
+-- @since 0.1.1.0
+module Data.Type.Predicate.Auto (
+    Auto(..)
+  , AutoElem(..)
+  , AutoProvable
+  ) where
+
+import           Data.List.NonEmpty        (NonEmpty(..))
+import           Data.Singletons
+import           Data.Type.Equality
+import           Data.Type.Predicate
+import           Data.Type.Predicate.Logic
+import           Data.Type.Universe
+
+-- | Automatically generate a witness for predicate @p@ applied to input
+-- @a@.
+--
+-- Mostly useful for situations where you know @a@ at compile-time, so you
+-- can just write 'auto' directly in your source code.  The choice is
+-- intended to mirror the @auto@ keyword in languages like Idris.
+--
+-- Very close in nature to the @Known@ typeclass in the /type-combinators/
+-- library.
+class Auto (p :: Predicate k) (a :: k) where
+    -- | Have the compiler generate a witness for @p \@\@ a@.
+    --
+    -- Must be called using type application syntax:
+    --
+    -- @
+    -- 'auto' @_ @p @a
+    -- @
+    auto :: p @@ a
+
+instance SingI a => Auto Evident a where
+    auto = sing
+
+instance Auto (EqualTo a) a where
+    auto = Refl
+
+instance (Auto p a, Auto q a) => Auto (p &&& q) a where
+    auto = (auto @_ @p @a, auto @_ @q @a)
+
+instance Auto q a => Auto (p ==> q) a where
+    auto _ = auto @_ @q @a
+
+-- | Helper "predicate transformer" that gives you an instant 'auto' for
+-- any 'Provable' instance.
+--
+-- For example, say you have predicate @P@ that you know is 'Provable', and
+-- you wish to generate a @P \@\@ x@, for some specific @x@ you know at
+-- compile-time.  You can use:
+--
+-- @
+-- 'auto' @_ @(AutoProvable P) @x
+-- @
+--
+-- to obtain a @P \@\@ x@.
+--
+-- 'AutoProvable' is essentially the identity function.
+data AutoProvable :: Predicate k -> Predicate k
+type instance Apply (AutoProvable p) a = p @@ a
+
+instance (Provable p, SingI a) => Auto (AutoProvable p) a where
+    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@.  
+--
+-- 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.
+--
+-- Used to help in the instance of 'Auto' for the 'In' predicate.
+--
+-- Example usage:
+--
+-- @
+-- autoElem :: Index '[1,6,2,3] 2
+-- -- IS (IS IZ)        -- third spot
+-- @
+--
+-- And when used with 'Auto':
+--
+-- @
+-- auto @_ @(In [] '[1,6,2,3]) @2
+-- -- IS (IS IZ)
+-- @
+class AutoElem f (as :: f k) (a :: k) where
+    -- | Generate the 'Elem' pointing to the @a :: @ in a type-level
+    -- collection @as :: f k@.
+    autoElem :: Elem f as a
+
+instance {-# OVERLAPPING #-} AutoElem [] (a ': as) a where
+    autoElem = IZ
+
+instance {-# OVERLAPPING #-} AutoElem [] as a => AutoElem [] (b ': as) a where
+    autoElem = IS autoElem
+
+instance AutoElem Maybe ('Just a) a where
+    autoElem = IsJust
+
+instance AutoElem (Either j) ('Right a) a where
+    autoElem = IsRight
+
+instance AutoElem NonEmpty (a ':| as) a where
+    autoElem = NEHead
+
+instance AutoElem [] as a => AutoElem NonEmpty (b ':| as) a where
+    autoElem = NETail autoElem
+
+instance AutoElem f as a => Auto (In f as) a where
+    auto = autoElem @f @as @a
+
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
@@ -76,12 +76,6 @@
 instance (Decidable p, Decidable q) => Decidable (p ||| q) where
     decide (x :: Sing a) = decideOr @p @q @a (decide @p x) (decide @q x)
 
--- | Picks the proof of @p@.  Note that this is instance has stronger
--- constraints than is strictly necessary; we should really only have to
--- require that either @p@ or @q@ is true.
-instance Provable p => Provable (p ||| q) where
-    prove x = Left (prove @p x)
-
 -- | Decide @p '|||' q@ based on decisions of @p@ and @q@.
 decideOr
     :: forall p q a. ()
@@ -137,6 +131,42 @@
         Disproved vq -> Disproved $ \vnpnq -> vpq (absurd . vnpnq vq)
 instance Provable (p ==> q) => Provable (Not q ==> Not p) where
     prove = contrapositive @p @q (prove @(p ==> q))
+
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> p) where
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Provable (p &&& q ==> p) where
+    prove = projAndFst @p @q
+
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Decidable (p &&& q ==> q) where
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Provable (p &&& q ==> q) where
+    prove = projAndSnd @p @q
+
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Decidable (p &&& p ==> p) where
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Provable (p &&& p ==> p) where
+    prove = projAndFst @p @p
+
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Decidable (p ==> p ||| q)
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Provable (p ==> p ||| q) where
+    prove = injOrLeft @p @q
+
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Decidable (q ==> p ||| q)
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Provable (q ==> p ||| q) where
+    prove = injOrRight @p @q
+
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Decidable (p ==> p ||| p)
+-- | @since 0.1.1.0
+instance {-# OVERLAPPING #-} Provable (p ==> p ||| p) where
+    prove = injOrLeft @p @p
 
 -- | @'Implies' p q@ is a constraint that @p '==>' q@ is 'Provable'; that
 -- is, you can prove that @p@ implies @q@.
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
@@ -35,7 +35,6 @@
   ) where
 
 import           Data.Singletons
-import           Data.Singletons.Decide
 import           Data.Singletons.Sigma
 import           Data.Type.Predicate
 import           Data.Type.Predicate.Logic
@@ -82,9 +81,10 @@
 type instance Apply (PPMap f p x) y = p (f @@ x) @@ y
 
 instance (Decidable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Decidable (Found (PPMap f p)) where
-    decide (x :: Sing a) = case decide @(Found p) ((sing :: Sing f) @@ x) of
-        Proved (i :&: p) -> Proved $ i :&: p
-        Disproved v      -> Disproved $ \case i :&: p -> v (i :&: p)
+    decide = mapDecision (\case i :&: p -> i :&: p)
+                         (\case i :&: p -> i :&: p)
+           . decide @(Found p)
+           . applySing (sing :: Sing f)     -- can just be sing @f in singletons 2.5, ghc 8.6+
 
 instance (Provable (Found (p :: ParamPred j v)), SingI (f :: k ~> j)) => Provable (Found (PPMap f p)) where
     prove (x :: Sing a) = case prove @(Found p) ((sing :: Sing f) @@ x) of
@@ -132,10 +132,9 @@
 type InP f = (ElemSym1 f :: ParamPred (f k) k)
 
 instance Universe f => Decidable (Found (InP f)) where
-    decide xs = case decide @(NotNull f) xs of
-      Proved (WitAny i s) -> Proved $ s :&: i
-      Disproved v         -> Disproved $ \case
-        s :&: i -> v $ WitAny i s
+    decide = mapDecision (\case WitAny i s -> s :&: i    )
+                         (\case s :&: i     -> WitAny i s)
+           . decide @(NotNull f)
 
 instance Decidable (NotNull f ==> Found (InP f))
 instance Provable (NotNull f ==> Found (InP f)) where
@@ -159,8 +158,6 @@
 type instance Apply (AnyMatch f p as) a = Any f (FlipPP p a) @@ as
 
 instance (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p)) where
-    decide xs = case decide @(Any f (Found p)) xs of
-      Proved (WitAny i (x :&: p)) -> Proved $ x :&: WitAny i p
-      Disproved v                 -> Disproved $ \case
-        x :&: WitAny i p -> v $ WitAny i (x :&: p)
-
+    decide = mapDecision (\case WitAny i (x :&: p) -> x :&: WitAny i p  )
+                         (\case x :&: WitAny i p   -> WitAny i (x :&: p))
+           . decide @(Any f (Found 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
@@ -67,7 +67,7 @@
 
 -- | @'In' f as@ is a predicate that a given input @a@ is a member of
 -- collection @as@.
-type In (f :: Type -> Type) (as :: f k) = TyCon1 (Elem f as)
+type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
 
 -- | A @'WitAny' p as@ is a witness that, for at least one item @a@ in the
 -- type-level collection @as@, the predicate @p a@ is true.
@@ -191,7 +191,7 @@
 -- In practice, this can be used to iterate and traverse and sequence
 -- actions over all "items" in @as@.
 genAllA
-    :: forall k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
+    :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h)
     => (forall a. Sing a -> h (p @@ a))        -- ^ predicate on value in context
     -> (Sing as -> h (All f p @@ as))               -- ^ predicate on collection in context
 genAllA f = igenAllA (const f)
@@ -221,7 +221,7 @@
 
 -- | Split a @'Sing' as@ into a proof that all @a@ in @as@ exist.
 splitSing
-    :: forall f (as :: f k). Universe f
+    :: forall f k (as :: f k). Universe f
     => Sing as
     -> All f (TyPred Sing) @@ as
 splitSing = igenAll @f @_ @(TyPred Sing) (\_ x -> x)
@@ -230,9 +230,10 @@
 pickElem
     :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k)
     => Decision (Elem f as a)
-pickElem = case decide @(Any f (TyPred ((:~:) a))) sing of
-    Proved (WitAny i Refl) -> Proved i
-    Disproved v            -> Disproved $ \i -> v $ WitAny i Refl
+pickElem = mapDecision (\case WitAny i Refl -> i)
+                       (\case i -> WitAny i Refl)
+         . decide @(Any f (TyPred ((:~:) a)))
+         $ sing
 
 -- | 'foldMapUni' but with access to the index.
 ifoldMapUni
@@ -294,7 +295,7 @@
         Disproved v -> Disproved $ \a -> v $ runWitAll a IZ
 
     igenAllA
-        :: forall (p :: k ~> Type) (as :: [k]) h. Applicative h
+        :: forall k (p :: k ~> Type) (as :: [k]) h. Applicative h
         => (forall a. Elem [] as a -> Sing a -> h (p @@ a))
         -> Sing as
         -> h (All [] p @@ as)
@@ -406,7 +407,7 @@
       Disproved v -> Disproved $ \a -> v $ runWitAll a NEHead
 
     igenAllA
-        :: forall (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h
+        :: forall k (p :: k ~> Type) (as :: NonEmpty k) h. Applicative h
         => (forall a. Elem NonEmpty as a -> Sing a -> h (p @@ a))
         -> Sing as
         -> h (All NonEmpty p @@ as)
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
@@ -75,6 +75,8 @@
 
 -- | Turn a 'Subset' into a list (or any 'Alternative') of satisfied
 -- predicates.
+--
+-- List is meant to include no duplicates.
 subsetToList
     :: forall f p t. (Universe f, Alternative t)
     => (Subset f p --># Any f p) t
@@ -156,13 +158,13 @@
 -- | Map a bidirectional implication over a subset described by that
 -- implication.
 --
--- Implication needs to be bidirection, or otherwise we can't produce
+-- Implication needs to be bidirectional, or otherwise we can't produce
 -- a /decidable/ subset as a result.
 mapSubset
     :: Universe f
     => (p --> q)
     -> (q --> p)
     -> (Subset f p --> Subset f q)
-mapSubset f g xs@Sing = withSingI xs $
+mapSubset f g xs = withSingI xs $
     imapSubset (\i -> f (index i xs))
                (\i -> g (index i xs))