diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,15 @@
 Changelog
 =========
 
+Version 0.1.3.1
+---------------
+
+*October 26, 2018*
+
+<https://github.com/mstksg/decidable/releases/tag/v0.1.3.1>
+
+*   *BUGFIX* Remove overlapping `Auto` instances for `IsNothing` and `IsLeft`.
+
 Version 0.1.3.0
 ---------------
 
@@ -13,6 +22,7 @@
 *   Added `Universe` instances (and appropriate `Elem` and `Auto` instances)
     for `Proxy` (the null universe) and `Identity`.
 *   `Auto` instances for `IsNothing` and `IsLeft`.
+
 
 Version 0.1.2.0
 ---------------
diff --git a/decidable.cabal b/decidable.cabal
--- a/decidable.cabal
+++ b/decidable.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5deeebc3dd1fcd483724e8469079eba0875cd3698198d81352d5b3bd6c2696ef
+-- hash: 8f4356d2d59f7c72a3fb5358dda90a0b36b47bb7fd03398fb1ed2c4c631a5a77
 
 name:           decidable
-version:        0.1.3.0
+version:        0.1.3.1
 synopsis:       Combinators for manipulating dependently-typed predicates.
 description:    This library provides combinators and typeclasses for working and manipulating
                 type-level predicates in Haskell, which are represented as matchable type-level
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
@@ -90,7 +90,7 @@
 --
 -- -- Then, write the 'Apply' instance, to specify the type of the
 -- -- witnesses of that predicate
--- instance 'Apply' (Not p) a = (p '@@' a) -> Void
+-- instance 'Apply' (Not p) a = (p '@@' a) -> 'Void'
 -- @
 --
 -- See the source of "Data.Type.Predicate" and "Data.Type.Predicate.Logic"
@@ -98,8 +98,8 @@
 -- always-true predicate 'Evident':
 --
 -- @
--- data Evident :: Predicate k
--- instance Apply Evident a = Sing a
+-- data Evident :: 'Predicate' k
+-- instance Apply Evident a = 'Sing' a
 -- @
 --
 -- And the "and" predicate combinator:
@@ -272,7 +272,7 @@
 -- function:
 --
 -- @
--- decideTC :: Sing a -> 'Decision' (T a)
+-- 'decideTC' :: 'Sing' a -> 'Decision' (T a)
 -- @
 --
 -- Is essentially 'Decidable', except with /type constructors/ @k ->
@@ -287,6 +287,10 @@
 
 -- | The canonical deciding function for @'DecidableTC' t@.
 --
+-- Note that because @t@ must be an injective type constructor, you can use
+-- this without explicit type applications; the instance of 'DecidableTC'
+-- can be inferred from the result type.
+--
 -- @since 0.1.1.0
 decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
 decideTC = decide @(TyPred t)
@@ -296,7 +300,7 @@
 -- function:
 --
 -- @
--- proveTC :: Sing a -> T a
+-- 'proveTC' :: 'Sing' a -> T a
 -- @
 --
 -- Is essentially 'Provable', except with /type constructors/ @k -> 'Type'@
@@ -310,6 +314,10 @@
 
 -- | The canonical proving function for @'DecidableTC' t@.
 --
+-- Note that because @t@ must be an injective type constructor, you can use
+-- this without explicit type applications; the instance of 'ProvableTC'
+-- can be inferred from the result type.
+--
 -- @since 0.1.1.0
 proveTC :: forall t a. ProvableTC t => Sing a -> t a
 proveTC = prove @(TyPred t)
@@ -355,7 +363,7 @@
 instance Provable (Not Impossible) where
     prove x v = absurd $ v x
 
--- | Decide @Not p@ based on decisions of @p@.
+-- | Decide @'Not' p@ based on decisions of @p@.
 decideNot
     :: forall p a. ()
     => Decision (p @@ a)
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
@@ -107,7 +107,7 @@
 -- compile-time.  You can use:
 --
 -- @
--- 'auto' @_ @(AutoProvable P) @x
+-- 'auto' \@_ \@('AutoProvable' P) \@x
 -- @
 --
 -- to obtain a @P \@\@ x@.
@@ -130,14 +130,14 @@
 -- Example usage:
 --
 -- @
--- autoElem :: Index '[1,6,2,3] 2
+-- 'autoElem' :: 'Index' '[1,6,2,3] 2
 -- -- IS (IS IZ)        -- third spot
 -- @
 --
 -- And when used with 'Auto':
 --
 -- @
--- auto @_ @(In [] '[1,6,2,3]) @2
+-- 'auto' \@_ \@('In' [] '[1,6,2,3]) \@2
 -- -- IS (IS IZ)
 -- @
 class AutoElem f (as :: f k) (a :: k) where
@@ -250,18 +250,10 @@
 instance SingI a => Auto IsJust ('Just a) where
     auto = WitAny IJust sing
 
--- | @since 0.1.3.0
-instance Auto IsNothing 'Nothing where
-    auto = \case WitAny i _ -> case i of {}
-
 -- | @since 0.1.2.0
 instance SingI a => Auto IsRight ('Right a) where
     auto = WitAny IRight sing
 
--- | @since 0.1.3.0
-instance Auto IsLeft ('Left a) where
-    auto = \case WitAny i _ -> case i of {}
-
 -- | @since 0.1.2.0
 instance SingI a => Auto (NotNull NonEmpty) (a ':| as) where
     auto = WitAny NEHead sing
@@ -270,9 +262,6 @@
 instance SingI a => Auto (NotNull ((,) j)) '(w, a) where
     auto = WitAny ISnd sing
 
-instance Auto (Null Proxy) 'Proxy where
-    auto = \case WitAny i _ -> case i of {}
-
 instance SingI a => Auto (NotNull Identity) ('Identity a) where
     auto = WitAny IId sing
 
@@ -282,8 +271,8 @@
 instance Auto (NotNull g) bs => Auto (NotNull (f :+: g)) ('InR bs) where
     auto = anySumR $ auto @_ @(NotNull g) @bs
 
--- | An @'AutoNot' p a@ constraint means that @p \@\@ a@ can be proven to not be
--- true at compiletime.
+-- | 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)
@@ -291,7 +280,7 @@
 -- | Disprove @p \@\@ a@ at compiletime.
 --
 -- @
--- autoNot @_ @p @a :: Not p @@ a
+-- 'autoNot' \@_ \@p \@a :: 'Not' p '@@' a
 -- @
 --
 -- @since 0.1.2.0