diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,10 @@
 # Revision history for boring
 
+## 0.1.2
+
+- Add instances for 'Boring' instances for 'SBool', 'SNat' and 'LE'.
+- Add 'Boring (Dec a)', 'boringYes' and 'boringNo'.
+
 ## 0.1.1
 
 - Add `GHC.Generics` instances
diff --git a/boring.cabal b/boring.cabal
--- a/boring.cabal
+++ b/boring.cabal
@@ -1,5 +1,5 @@
 name:               boring
-version:            0.1.1
+version:            0.1.2
 synopsis:           Boring and Absurd types
 description:
   * @Boring@ types are isomorphic to @()@.
@@ -14,7 +14,7 @@
 license-file:       LICENSE
 author:             Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>
-copyright:          (c) 2017 Oleg Grenrus
+copyright:          (c) 2017-2019 Oleg Grenrus
 category:           Data
 build-type:         Simple
 extra-source-files: ChangeLog.md
@@ -31,10 +31,12 @@
   build-depends:
       adjunctions          >=4.4     && <4.5
     , base                 >=4.7     && <4.13
-    , base-compat          >=0.10.5 && <0.11
-    , constraints          ==0.4.1.3 || >=0.10 && <0.11
-    , fin                  >=0.0.1   && <0.1
-    , generics-sop         >=0.3.2.0 && <0.5
+    , base-compat          >=0.10.5  && <0.11
+    , constraints          ==0.4.1.3 || >=0.10 && <0.12
+    , dec                  >=0.0.3   && <0.1
+    , fin                  >=0.0.3   && <0.1
+    , generics-sop         >=0.3.2.0 && <0.6
+    , singleton-bool       >=0.1.4   && <0.2
     , streams              >=3.3     && <3.4
     , tagged               >=0.8.6   && <0.9
     , transformers         >=0.3     && <0.6
@@ -42,7 +44,7 @@
     , vec                  >=0.1     && <0.2
 
   if !impl(ghc >=8.0)
-    build-depends: semigroups >=0.18.5 && <0.19
+    build-depends: semigroups >=0.18.5 && <0.20
 
   if !impl(ghc >=7.10)
     build-depends: void >=0.7.2 && <0.8
diff --git a/src/Data/Boring.hs b/src/Data/Boring.hs
--- a/src/Data/Boring.hs
+++ b/src/Data/Boring.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE GADTs            #-}
 {-# LANGUAGE TypeOperators    #-}
 {-# LANGUAGE ConstraintKinds  #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE UndecidableInstances #-}
 -- | 'Boring' and 'Absurd' classes. One approach.
 --
@@ -54,12 +55,17 @@
     -- * Classes
     Boring (..),
     Absurd (..),
-    -- * More integeresting stuff
+    -- * More interesting stuff
     vacuous,
     boringRep,
     untainted,
     devoid,
     united,
+    -- ** Dec
+    --
+    -- | @'Dec' a@ can be 'Boring' in two ways: When 'a' is 'Boring' or 'Absurd'.
+    boringYes,
+    absurdNo,
     ) where
 
 import Prelude ()
@@ -75,15 +81,20 @@
 import Data.List.NonEmpty    (NonEmpty (..))
 import Data.Proxy            (Proxy (..))
 import Data.Tagged           (Tagged (..))
+import Data.Type.Dec         (Dec (..), Decidable (..))
 import Data.Stream.Infinite  (Stream (..))
 import GHC.Generics   hiding (Rep)
 
-import qualified Data.Fin      as Fin
-import qualified Data.Nat      as Nat
-import qualified Data.Vec.Lazy as Vec
-import qualified Data.Vec.Pull as Vec.Pull
-import qualified Data.Void     as V
-import qualified Generics.SOP  as SOP
+import qualified Data.Fin                  as Fin
+import qualified Data.Nat                  as Nat
+import qualified Data.Singletons.Bool      as Bool
+import qualified Data.Type.Nat             as Nat
+import qualified Data.Type.Nat.LE          as ZeroSucc
+import qualified Data.Type.Nat.LE.ReflStep as ReflStep
+import qualified Data.Vec.Lazy             as Vec
+import qualified Data.Vec.Pull             as Vec.Pull
+import qualified Data.Void                 as V
+import qualified Generics.SOP              as SOP
 
 #if MIN_VERSION_base(4,7,0)
 import qualified Data.Coerce        as Co
@@ -199,6 +210,10 @@
 # endif
 #endif
 
+-------------------------------------------------------------------------------
+-- vec + fin + singleton-bool
+-------------------------------------------------------------------------------
+
 instance n ~ 'Nat.Z => Boring (Vec.Vec n a) where
     boring = Vec.empty
 
@@ -208,6 +223,28 @@
 instance n ~ ('Nat.S 'Nat.Z) => Boring (Fin.Fin n) where
     boring = Fin.boring
 
+-- singletons are boring
+
+-- | @since 0.1.3
+instance Nat.SNatI n => Boring (Nat.SNat n) where
+    boring = Nat.snat
+
+-- | @since 0.1.3
+instance Bool.SBoolI b => Boring (Bool.SBool b) where
+    boring = Bool.sbool
+
+-- | @since 0.1.3
+instance ZeroSucc.LE n m => Boring (ZeroSucc.LEProof n m) where
+    boring = ZeroSucc.leProof
+
+-- | @since 0.1.3
+instance (ZeroSucc.LE n m, Nat.SNatI m) => Boring (ReflStep.LEProof n m) where
+    boring = ReflStep.fromZeroSucc ZeroSucc.leProof
+
+-------------------------------------------------------------------------------
+-- Generics
+-------------------------------------------------------------------------------
+
 instance Boring (U1 p) where
     boring = U1
 
@@ -280,6 +317,16 @@
 instance n ~ 'Nat.Z => Absurd (Fin.Fin n) where
     absurd = Fin.absurd
 
+instance (ZeroSucc.LE m n, n' ~ 'Nat.S n) => Absurd (ZeroSucc.LEProof n' m) where
+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof
+
+instance (ZeroSucc.LE m n, n' ~ 'Nat.S n, Nat.SNatI n) => Absurd (ReflStep.LEProof n' m) where
+    absurd = ZeroSucc.leSwap' ZeroSucc.leProof . ReflStep.toZeroSucc
+
+-------------------------------------------------------------------------------
+-- Generics
+-------------------------------------------------------------------------------
+
 instance Absurd (V1 p) where
     absurd v = case v of {}
 
@@ -337,3 +384,25 @@
 -- @
 united :: (Boring a, Functor f) => (a -> f a) -> s -> f s
 united f v = v <$ f boring
+
+-------------------------------------------------------------------------------
+-- Dec
+-------------------------------------------------------------------------------
+
+-- | This relies on the fact that @a@ is /proposition/ in h-Prop sense.
+--
+-- @since 0.1.3
+instance Decidable a => Boring (Dec a) where
+    boring = decide
+
+-- | 'Yes', it's 'boring'.
+--
+-- @since 0.1.3
+boringYes :: Boring a => Dec a
+boringYes = Yes boring
+
+-- | 'No', it's 'absurd'.
+--
+-- @since 0.1.3
+absurdNo :: Absurd a => Dec a
+absurdNo = No absurd