diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -25,8 +25,7 @@
                           (:-$), (:-$$), (:-$$$),
                           (%:-), (%-),
                           -- ** Type-level predicate & judgements
-                          Leq(..), (:<=),
-                          LeqInstance,
+                          Leq(..), (:<=), LeqInstance,
                           boolToPropLeq, boolToClassLeq, propToClassLeq,
                           propToBoolLeq,
                           -- * Conversion functions
@@ -35,10 +34,10 @@
                           nat, snat,
                           -- * Properties of natural numbers
                           IsPeano(..),
-                          plusCongR, plusCongL, snEqZAbsurd,
-                          plusInjectiveL, plusInjectiveR,
-                          multCongL, multCongR,
-                          plusMinusEqL, leqRhs, leqLhs,
+                          plusCong, plusCongR, plusCongL,
+                          snEqZAbsurd, plusInjectiveL, plusInjectiveR,
+                          multCongL, multCongR, multCong,
+                          plusMinusEqL,
                           plusNeutralR, plusNeutralL,
                           -- * Properties of ordering 'Leq'
                           PeanoOrder(..),
@@ -65,11 +64,6 @@
 import Data.Type.Natural.Class hiding (One, Zero, sOne, sZero)
 import Data.Type.Natural.Core
 import Data.Type.Natural.Definitions hiding ((:<=))
-
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-import Data.Kind
-#endif
-
 import Data.Singletons
 import Data.Singletons.Prelude.Ord
 import Data.Singletons.Decide
@@ -114,7 +108,8 @@
 --------------------------------------------------
 
 -- | Since 0.5.0.0
-instance IsPeano ('KProxy :: KProxy Nat) where
+instance IsPeano Nat where
+  {-# SPECIALISE instance IsPeano Nat #-}
   induction base _step SZ = base
   induction base step (SS n) = step n (induction base step n)
 
@@ -154,18 +149,6 @@
     === m %:+ l   `because` eq
     === l %:+ m   `because` plusComm m l
 
--- eqSuccMinus :: ((m :<<= n) ~ 'True)
---             => SNat n -> SNat m -> ('S n :-: m) :~: ('S (n :-: m))
--- eqSuccMinus _      SZ     = Refl
--- eqSuccMinus (SS n) (SS m) =
---   start (SS (SS n) %:- SS m)
---     =~= SS n %:- m
---     === SS (n %:- m)       `because` eqSuccMinus n m
---     =~= SS (SS n %:- SS m)
--- #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800
--- eqSuccMinus _ _ = bugInGHC
--- #endif
-
 reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n :== m)
 reflToSEqual SZ     _      Refl = Witness
 reflToSEqual (SS n) (SS m) Refl =
@@ -217,7 +200,8 @@
             STrue  -> Refl
             SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {}
 
-instance PeanoOrder ('KProxy :: KProxy Nat) where
+instance PeanoOrder Nat where
+  {-# SPECIALISE instance PeanoOrder Nat #-}
   leqZero _ = Witness
   leqSucc _      _      Witness = Witness
   viewLeq SZ     n      Witness = LeqZero n
@@ -228,9 +212,6 @@
     case n %:== m of
       SFalse -> case n %:<= m of
         STrue -> Witness
-        _ -> bugInGHC
-      _ -> bugInGHC
-
   eqlCmpEQ n m Refl =
     case n %:== m of
       STrue  -> Refl
diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs
--- a/Data/Type/Natural/Builtin.hs
+++ b/Data/Type/Natural/Builtin.hs
@@ -27,13 +27,11 @@
        )
        where
 import Data.Type.Natural.Class
-import Data.Type.Natural.Compat
 
 import           Data.Singletons.Decide       (SDecide (..))
 import           Data.Singletons.Decide       (Decision (..))
-import           Data.Singletons.Prelude      (PNum (..), SNum (..), Sing (..))
+import           Data.Singletons.Prelude      (SNum (..), PNum(..), Sing (..))
 import           Data.Singletons.Prelude      (SingI (..))
-import           Data.Singletons.Prelude      (KProxy (..))
 import           Data.Singletons.Prelude      (SingKind (..), SomeSing (..))
 import           Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..))
 import           Data.Singletons.Prelude.Ord  (POrd (..), SOrd (..))
@@ -53,9 +51,6 @@
 import           Proof.Equational             (because)
 import           Proof.Propositional          (Empty (..), IsTrue (..))
 import           Unsafe.Coerce                (unsafeCoerce)
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-import Data.Kind
-#endif
 
 -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@.
 type Peano = PN.Nat
@@ -142,7 +137,7 @@
 fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :~: Succ (FromPeano n)
 fromPeanoSuccCong _sn = Refl
 
-fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :~: FromPeano n :+ FromPeano m
+fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n :+ m) :~: FromPeano n :+ FromPeano m
 fromPeanoPlusCong SZ _ = Refl
 fromPeanoPlusCong (SS sn) sm =
   start (sFromPeano (SS sn %:+ sm))
@@ -152,7 +147,7 @@
     =~= sSucc (sFromPeano sn) %:+ sFromPeano sm
     =~= sFromPeano (SS sn)    %:+ sFromPeano sm
 
-toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n :+ m) :~: ToPeano n :+ ToPeano m
+toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :~: ToPeano n :+ ToPeano m
 toPeanoPlusCong sn sm =
   case viewNat sn of
     IsZero -> Refl
@@ -287,7 +282,8 @@
     IsSucc sl -> step (inductionNat base step sl)
 
 
-instance IsPeano ('KProxy :: KProxy TL.Nat) where
+instance IsPeano TL.Nat where
+  {-# SPECIALISE instance IsPeano TL.Nat #-}
   predSucc _ = Refl
   plusMinus _ _ = Refl
   succInj Refl = Refl
@@ -344,7 +340,8 @@
   MyLeqHelper n m 'EQ = 'True
   MyLeqHelper n m 'GT = 'False
 
-instance PeanoOrder ('KProxy :: KProxy TL.Nat) where
+instance PeanoOrder TL.Nat where
+  {-# SPECIALISE instance PeanoOrder TL.Nat #-}
   eqlCmpEQ _ _ Refl = Refl
   ltToLeq _ _ Refl = Witness
   succLeqToLT m n Witness =
diff --git a/Data/Type/Natural/Class/Arithmetic.hs b/Data/Type/Natural/Class/Arithmetic.hs
--- a/Data/Type/Natural/Class/Arithmetic.hs
+++ b/Data/Type/Natural/Class/Arithmetic.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-}
 {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies            #-}
-{-# LANGUAGE ViewPatterns                                                  #-}
+{-# LANGUAGE TypeInType, ViewPatterns                                      #-}
 module Data.Type.Natural.Class.Arithmetic
        (Zero, One, S, sZero, sOne, ZeroOrSucc(..),
         plusCong, plusCongR, plusCongL, succCong,
@@ -18,21 +18,21 @@
 import Proof.Equational
 import Proof.Propositional
 
-type family Zero (kproxy :: KProxy nat) :: nat where
-  Zero 'KProxy = FromInteger 0
+type family Zero nat :: nat where
+  Zero nat = FromInteger 0
 
-sZero :: (SNum kproxy) => Sing (Zero kproxy)
+sZero :: (SNum nat) => Sing (Zero nat)
 sZero = sFromInteger (sing :: Sing 0)
 
-type family One (kproxy :: KProxy nat) :: nat where
-  One 'KProxy = FromInteger 1
+type family One nat :: nat where
+  One nat = FromInteger 1
 
-sOne :: SNum kproxy => Sing (One kproxy)
+sOne :: SNum nat => Sing (One nat)
 sOne = sFromInteger (sing :: Sing 1)
 
 type S n = Succ n
 
-sS :: SEnum ('KProxy :: KProxy nat) => Sing (n :: nat) -> Sing (S n)
+sS :: SEnum nat => Sing (n :: nat) -> Sing (S n)
 sS = sSucc
 
 predCong :: n :~: m -> Pred n :~: Pred m
@@ -69,7 +69,7 @@
 minusCongR _ Refl = Refl
 
 data ZeroOrSucc (n :: nat) where
-  IsZero :: ZeroOrSucc (Zero 'KProxy)
+  IsZero :: ZeroOrSucc (Zero nat)
   IsSucc :: Sing n -> ZeroOrSucc (Succ n)
 
 newtype Assoc op n = Assoc { assocProof :: forall k l. Sing k -> Sing l ->
@@ -81,11 +81,11 @@
 newtype IdentityR op e (n :: nat) = IdentityR { idRProof :: Apply (op n) e :~: n }
 newtype IdentityL op e (n :: nat) = IdentityL { idLProof :: Apply (op e) n :~: n }
 
-type PlusZeroR (n :: nat) = IdentityR (:+$$) (Zero 'KProxy) n
+type PlusZeroR (n :: nat) = IdentityR (:+$$) (Zero nat) n
 newtype PlusSuccR (n :: nat) =
   PlusSuccR { plusSuccRProof :: forall m. Sing m -> n :+ S m :~: S (n :+ m) }
 
-type PlusZeroL (n :: nat) = IdentityL (:+$$) (Zero 'KProxy) n
+type PlusZeroL (n :: nat) = IdentityL (:+$$) (Zero nat) n
 newtype PlusSuccL (m :: nat) =
   PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n :+ m :~: S (n :+ m) }
 
@@ -93,48 +93,48 @@
 
 type PlusComm = Comm (:+$$)
 
-data MultZeroL n =
-  MultZeroL { multZeroLProof :: !(Zero ('KProxy :: KProxy nat) :* n :~: Zero 'KProxy) }
-data MultZeroR (n :: nat) =
-  MultZeroR { multZeroRProof :: !(n :* Zero ('KProxy :: KProxy nat) :~: Zero 'KProxy) }
+newtype MultZeroL (n :: nat) =  MultZeroL { multZeroLProof :: Zero nat :* n :~: Zero nat }
+newtype MultZeroR (n :: nat) =
+  MultZeroR { multZeroRProof :: n :* Zero nat :~: Zero nat }
 
 newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n :* m :~: n :* m :+ m }
-data MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n :* S m :~: n :* m :+ n }
+newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n :* S m :~: n :* m :+ n }
 
-data PlusMultDistrib n =
+newtype PlusMultDistrib (n :: nat) =
   PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l
                                          -> (n :+ m) :* l :~: n :* l :+ m :* l
                   }
 
-newtype PlusEqCancelL n = PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l
+newtype PlusEqCancelL (n :: nat) =
+  PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l
                                                        -> n :+ m :~: n :+ l -> m :~: l }
 
-data SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: !(Succ n :~: One 'KProxy :+ n) }
+newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat :+ n }
 newtype MultEqCancelR n =
   MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l
                                         -> n :* Succ l :~: m :* Succ l
                                         -> n :~: m
                 }
 
-class (SDecide kproxy, SNum kproxy, SEnum kproxy, kproxy ~ 'KProxy)
-    => IsPeano (kproxy :: KProxy nat) where
+class (SDecide nat, SNum nat, SEnum nat, nat ~ nat)
+    => IsPeano nat where
   {-# MINIMAL succOneCong, succNonCyclic, predSucc, plusMinus,
               succInj, ( (plusZeroL, plusSuccL) | (plusZeroR, plusZeroL))
                      , ( (multZeroL, multSuccL) | (multZeroR, multSuccR)),
               induction #-}
 
-  succOneCong   :: Succ (Zero kproxy) :~: One kproxy
+  succOneCong   :: Succ (Zero nat) :~: One nat
   succInj       :: Succ n :~: Succ (m :: nat) -> n :~: m
   succInj'      :: proxy n -> proxy' m -> Succ n :~: Succ (m :: nat) -> n :~: m
   succInj' _ _  = succInj
-  succNonCyclic :: Sing n -> Succ n :~: Zero kproxy -> Void
-  induction     :: p (Zero kproxy) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k
+  succNonCyclic :: Sing n -> Succ n :~: Zero nat -> Void
+  induction     :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k
   plusMinus :: Sing (n :: nat) -> Sing m -> n :+ m :- m :~: n
 
-  plusZeroL :: Sing n -> (Zero kproxy :+ n) :~: n
+  plusZeroL :: Sing n -> (Zero nat :+ n) :~: n
   plusZeroL sn = idLProof (induction base step sn)
     where
-      base :: PlusZeroL (Zero kproxy)
+      base :: PlusZeroL (Zero nat)
       base = IdentityL (plusZeroR sZero)
 
       step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n)
@@ -146,7 +146,7 @@
   plusSuccL :: Sing n -> Sing m -> S n :+ m :~: S (n :+ m :: nat)
   plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0
     where
-      base :: PlusSuccL (Zero kproxy)
+      base :: PlusSuccL (Zero nat)
       base = PlusSuccL $ \sn ->
         start (sS sn %:+ sZero)
           === sS sn             `because` plusZeroR (sS sn)
@@ -159,10 +159,10 @@
         === sS (sS (sn %:+ sm)) `because` succCong (ih sn)
         === sS (sn %:+ sS sm)   `because` succCong (sym $ plusSuccR sn sm)
 
-  plusZeroR :: Sing n -> (n :+ Zero kproxy) :~: n
+  plusZeroR :: Sing n -> (n :+ Zero nat) :~: n
   plusZeroR sn = idRProof (induction base step sn)
     where
-      base :: PlusZeroR (Zero kproxy)
+      base :: PlusZeroR (Zero nat)
       base = IdentityR (plusZeroL sZero)
 
       step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n)
@@ -174,7 +174,7 @@
   plusSuccR :: Sing n -> Sing m -> n :+ S m :~: S (n :+ m :: nat)
   plusSuccR sn0 = plusSuccRProof (induction base step sn0)
     where
-      base :: PlusSuccR (Zero kproxy)
+      base :: PlusSuccR (Zero nat)
       base = PlusSuccR $ \sk ->
         start (sZero %:+ sS sk)
           === sS sk             `because` plusZeroL (sS sk)
@@ -190,7 +190,7 @@
   plusComm  :: Sing n -> Sing m -> n :+ m :~: (m :: nat) :+ n
   plusComm sn0 = commProof (induction base step sn0)
     where
-      base :: PlusComm (Zero kproxy)
+      base :: PlusComm (Zero nat)
       base = Comm $ \sk ->
         start (sZero %:+ sk)
           === sk             `because` plusZeroL sk
@@ -207,7 +207,7 @@
             -> (n :+ m) :+ l :~: n :+ (m :+ l)
   plusAssoc sn m l = assocProof (induction base step sn) m l
     where
-      base :: Assoc (:+$$) (Zero kproxy)
+      base :: Assoc (:+$$) (Zero nat)
       base = Assoc $ \ sk sl ->
         start ((sZero %:+ sk) %:+ sl)
           === sk %:+ sl
@@ -224,10 +224,10 @@
         ===   sS sk %:+ (sl %:+ su)   `because` sym (plusSuccL sk (sl %:+ su))
 
 
-  multZeroL :: Sing n -> Zero kproxy :* n :~: Zero kproxy
+  multZeroL :: Sing n -> Zero nat :* n :~: Zero nat
   multZeroL sn0 = multZeroLProof $ induction base step sn0
     where
-      base :: MultZeroL (Zero kproxy)
+      base :: MultZeroL (Zero nat)
       base = MultZeroL (multZeroR sZero)
 
       step :: Sing (k :: nat) -> MultZeroL k ->  MultZeroL (S k)
@@ -240,7 +240,7 @@
   multSuccL :: Sing (n :: nat) -> Sing m -> S n :* m :~: n :* m :+ m
   multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0
     where
-      base :: MultSuccL (Zero kproxy)
+      base :: MultSuccL (Zero nat)
       base = MultSuccL $ \sk ->
         start (sS sk %:* sZero)
           === sZero                  `because` multZeroR (sS sk)
@@ -266,10 +266,10 @@
               `because` succCong (plusCongL (sym $ multSuccR sk sm) sm)
           === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm)
 
-  multZeroR :: Sing n -> n :* Zero kproxy :~: Zero kproxy
+  multZeroR :: Sing n -> n :* Zero nat :~: Zero nat
   multZeroR sn0 = multZeroRProof $ induction base step sn0
     where
-      base :: MultZeroR (Zero kproxy)
+      base :: MultZeroR (Zero nat)
       base = MultZeroR (multZeroR sZero)
 
       step :: Sing (k :: nat) -> MultZeroR k ->  MultZeroR (S k)
@@ -282,7 +282,7 @@
   multSuccR :: Sing n -> Sing m -> n :* S m :~: n :* m :+ (n :: nat)
   multSuccR sn0 = multSuccRProof $ induction base step sn0
     where
-      base :: MultSuccR (Zero kproxy)
+      base :: MultSuccR (Zero nat)
       base = MultSuccR $ \sk ->
         start (sZero %:* sS sk)
           === sZero
@@ -317,7 +317,7 @@
   multComm  :: Sing (n :: nat) -> Sing m -> n :* m :~: m :* n
   multComm sn0 = commProof (induction base step sn0)
     where
-      base :: Comm (:*$$) (Zero kproxy)
+      base :: Comm (:*$$) (Zero nat)
       base = Comm $ \sk ->
         start (sZero %:* sk)
           === sZero           `because` multZeroL sk
@@ -330,7 +330,7 @@
           === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk
           === sk %:* sS sn     `because` sym (multSuccR sk sn)
 
-  multOneR :: Sing n -> n :* One kproxy :~: n
+  multOneR :: Sing n -> n :* One nat :~: n
   multOneR sn =
     start (sn %:* sOne)
       === sn %:* sS sZero      `because` multCongR sn (sym $ succOneCong)
@@ -338,7 +338,7 @@
       === sZero %:+ sn         `because` plusCongL (multZeroR sn) sn
       === sn                   `because` plusZeroL sn
 
-  multOneL :: Sing n -> One kproxy :* n :~: n
+  multOneL :: Sing n -> One nat :* n :~: n
   multOneL sn =
     start (sOne %:* sn)
       === sn %:* sOne   `because` multComm sOne sn
@@ -348,7 +348,7 @@
                 -> (n :+ m) :* l :~: n :* l :+ m :* l
   plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0
     where
-      base :: PlusMultDistrib (Zero kproxy)
+      base :: PlusMultDistrib (Zero nat)
       base = PlusMultDistrib $ \sk sl ->
         start ((sZero %:+ sk) %:* sl)
           === (sk %:* sl)
@@ -377,7 +377,7 @@
       === m %:* n %:+ l %:* n `because` plusMultDistrib m l n
       === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n)
 
-  minusNilpotent :: Sing n -> n :- n :~: Zero kproxy
+  minusNilpotent :: Sing n -> n :- n :~: Zero nat
   minusNilpotent n =
     start (n %:- n)
       === (sZero %:+ n) %:- n  `because` minusCongL (sym $ plusZeroL n) n
@@ -388,7 +388,7 @@
             -> (n :* m) :* l :~: n :* (m :* l)
   multAssoc sn0 = assocProof $ induction base step sn0
     where
-      base :: Assoc (:*$$) (Zero kproxy)
+      base :: Assoc (:*$$) (Zero nat)
       base = Assoc $ \ m l ->
         start (sZero %:* m %:* l)
           === sZero %:* l  `because` multCongL (multZeroL m) l
@@ -406,7 +406,7 @@
   plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ m :~: n :+ l -> m :~: l
   plusEqCancelL = plusEqCancelLProof . induction base step
     where
-      base :: PlusEqCancelL (Zero kproxy)
+      base :: PlusEqCancelL (Zero nat)
       base = PlusEqCancelL $ \l m nlnm ->
         start l === sZero %:+ l `because` sym (plusZeroL l)
                 === sZero %:+ m `because` nlnm
@@ -429,10 +429,10 @@
       === (m %:+ l) `because` nlml
       === (l %:+ m) `because` plusComm m l
 
-  succAndPlusOneL :: Sing n -> Succ n :~: One kproxy :+ n
+  succAndPlusOneL :: Sing n -> Succ n :~: One nat :+ n
   succAndPlusOneL = proofSuccPlusL . induction base step
     where
-      base :: SuccPlusL (Zero kproxy)
+      base :: SuccPlusL (Zero nat)
       base = SuccPlusL $
              start (sSucc sZero)
                === sOne           `because` succOneCong
@@ -444,7 +444,7 @@
           === sSucc (sOne %:+ sn) `because` succCong ih
           === sOne %:+ sSucc sn   `because` sym (plusSuccR sOne sn)
 
-  succAndPlusOneR :: Sing n -> Succ n :~: n :+ One kproxy
+  succAndPlusOneR :: Sing n -> Succ n :~: n :+ One nat
   succAndPlusOneR n =
     start (sSucc n)
       === sOne %:+ n `because` succAndPlusOneL n
@@ -458,13 +458,13 @@
       base = IsZero
       step sn _ = IsSucc sn
 
-  plusEqZeroL :: Sing n -> Sing m -> n :+ m :~: Zero kproxy -> n :~: Zero kproxy
+  plusEqZeroL :: Sing n -> Sing m -> n :+ m :~: Zero nat -> n :~: Zero nat
   plusEqZeroL n m Refl =
     case zeroOrSucc n of
       IsZero -> Refl
       IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m)
 
-  plusEqZeroR :: Sing n -> Sing m -> n :+ m :~: Zero kproxy -> m :~: Zero kproxy
+  plusEqZeroR :: Sing n -> Sing m -> n :+ m :~: Zero nat -> m :~: Zero nat
   plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n)
 
   predUnique :: Sing (n :: nat) -> Sing m -> Succ n :~: m -> n :~: Pred m
@@ -487,7 +487,7 @@
   multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m
   multEqCancelR = proofMultEqCancelR . induction base step
     where
-      base :: MultEqCancelR (Zero kproxy)
+      base :: MultEqCancelR (Zero nat)
       base = MultEqCancelR $ \m l zslmsl ->
         sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero
           === sZero %:* l            `because` sym (multZeroL l)
@@ -512,7 +512,7 @@
                     === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l)
         in succCong pf' `trans` sym sm'Em
 
-  succPred :: Sing n -> (n :~: Zero kproxy -> Void) -> Succ (Pred n) :~: n
+  succPred :: Sing n -> (n :~: Zero nat -> Void) -> Succ (Pred n) :~: n
   succPred n nonZero =
     case zeroOrSucc n of
       IsZero -> absurd $ nonZero Refl
@@ -534,8 +534,10 @@
 refute [t| 'GT :~: 'EQ |]
 refute [t| 'True :~: 'False |]
 
+pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n
 pattern Zero <- (zeroOrSucc -> IsZero) where
   Zero = sZero
 
+pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n
 pattern Succ n <- (zeroOrSucc -> IsSucc n) where
   Succ n = sSucc n
diff --git a/Data/Type/Natural/Class/Order.hs b/Data/Type/Natural/Class/Order.hs
--- a/Data/Type/Natural/Class/Order.hs
+++ b/Data/Type/Natural/Class/Order.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts        #-}
-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-}
-{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies            #-}
+{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts         #-}
+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                       #-}
+{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes  #-}
+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}
 module Data.Type.Natural.Class.Order
        (PeanoOrder(..), DiffNat(..), LeqView(..),
         FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,
@@ -19,7 +19,7 @@
 import Proof.Propositional
 
 data LeqView (n :: nat) (m :: nat) where
-  LeqZero :: Sing n -> LeqView (Zero 'KProxy) n
+  LeqZero :: Sing n -> LeqView (Zero nat) n
   LeqSucc :: Sing n -> Sing m -> IsTrue (n :<= m) -> LeqView (Succ n) (Succ m)
 
 data DiffNat n m where
@@ -28,15 +28,15 @@
 newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n :<= m) -> DiffNat n m }
 newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m) }
 
-succDiffNat :: IsPeano ('KProxy :: KProxy nat)
+succDiffNat :: IsPeano nat
             => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m)
 succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m
 
-coerceLeqL :: forall (n :: nat) m l . IsPeano ('KProxy :: KProxy nat) => n :~: m -> Sing l
+coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l
            -> IsTrue (n :<= l) -> IsTrue (m :<= l)
 coerceLeqL Refl _ Witness = Witness
 
-coerceLeqR :: forall (n :: nat) m l . IsPeano ('KProxy :: KProxy nat) =>  Sing l -> n :~: m
+coerceLeqR :: forall (n :: nat) m l . IsPeano nat =>  Sing l -> n :~: m
            -> IsTrue (l :<= n) -> IsTrue (l :<= m)
 coerceLeqR _ Refl Witness = Witness
 
@@ -71,7 +71,7 @@
 
 newtype LeqViewRefl n = LeqViewRefl { proofLeqViewRefl :: LeqView n n }
 
-class (SOrd kproxy, IsPeano kproxy) => PeanoOrder (kproxy :: KProxy nat) where
+class (SOrd nat, IsPeano nat) => PeanoOrder nat where
   {-# MINIMAL ( succLeqToLT, cmpZero, leqRefl
               | leqZero, leqSucc , viewLeq
               | leqWitness, leqStep
@@ -133,7 +133,7 @@
   ltToSuccLeq n m nLTm =
      leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm)
 
-  cmpZero :: Sing a -> Compare (Zero kproxy) (Succ a) :~: 'LT
+  cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: 'LT
   cmpZero sn = leqToLT sZero (sSucc sn) $ leqStep (sSucc sZero) (sSucc sn) sn $
                start (sSucc sZero %:+ sn)
                  === sSucc (sZero %:+ sn) `because` plusSuccL sZero sn
@@ -147,13 +147,13 @@
       === sFlipOrdering SLT            `because` congFlipOrdering (leqToLT b a sbLEQa)
       =~= SGT
 
-  cmpZero' :: Sing a -> Either (Compare (Zero kproxy) a :~: 'EQ) (Compare (Zero kproxy) a :~: 'LT)
+  cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: 'EQ) (Compare (Zero nat) a :~: 'LT)
   cmpZero' n =
     case zeroOrSucc n of
       IsZero    -> Left $ eqlCmpEQ sZero n Refl
       IsSucc n' -> Right $ cmpZero n'
 
-  zeroNoLT :: Sing a -> Compare a (Zero kproxy) :~: 'LT -> Void
+  zeroNoLT :: Sing a -> Compare a (Zero nat) :~: 'LT -> Void
   zeroNoLT n eql =
     case cmpZero' n of
       Left cmp0nEQ -> eliminate $
@@ -207,8 +207,8 @@
   ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: 'LT
   ltSucc = proofLTSucc . induction base step
     where
-      base :: LTSucc (Zero kproxy)
-      base = LTSucc $ cmpZero (sZero :: Sing (Zero kproxy))
+      base :: LTSucc (Zero nat)
+      base = LTSucc $ cmpZero (sZero :: Sing (Zero nat))
 
       step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n)
       step n (LTSucc ih) = LTSucc $
@@ -220,7 +220,7 @@
                -> Compare n (Succ m) :~: 'LT
   cmpSuccStepR = proofCmpSuccStepR . induction base step
     where
-      base :: CmpSuccStepR (Zero kproxy)
+      base :: CmpSuccStepR (Zero nat)
       base = CmpSuccStepR $ \m _ -> cmpZero m
 
       step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n)
@@ -254,7 +254,7 @@
           === SLT `because` ltSucc n
       Right nLTm -> ltSuccLToLT n m nLTm
 
-  leqZero :: Sing n -> IsTrue (Zero kproxy :<= n)
+  leqZero :: Sing n -> IsTrue (Zero nat :<= n)
   leqZero sn =
     case zeroOrSucc sn of
       IsZero   -> leqRefl sn
@@ -273,7 +273,7 @@
   leqViewRefl :: Sing (n :: nat) -> LeqView n n
   leqViewRefl = proofLeqViewRefl . induction base step
     where
-      base :: LeqViewRefl (Zero kproxy)
+      base :: LeqViewRefl (Zero nat)
       base = LeqViewRefl $ LeqZero sZero
       step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n)
       step n (LeqViewRefl nLEQn) =
@@ -293,7 +293,7 @@
   leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> DiffNat n m
   leqWitness = leqWitPf . induction base step
     where
-      base :: LeqWitPf (Zero kproxy)
+      base :: LeqWitPf (Zero nat)
       base = LeqWitPf $ \sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm
 
       step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n)
@@ -306,7 +306,7 @@
   leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m)
   leqStep = leqStepPf . induction base step
     where
-      base :: LeqStepPf (Zero kproxy)
+      base :: LeqStepPf (Zero nat)
       base = LeqStepPf $ \k _ _ -> leqZero k
 
       step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n)
@@ -394,7 +394,7 @@
                  `because` sym (plusAssoc n mMINn k)
              =~= m %:+ k
 
-  leqZeroElim :: Sing n -> IsTrue (n :<= Zero kproxy) -> n :~: Zero kproxy
+  leqZeroElim :: Sing n -> IsTrue (n :<= Zero nat) -> n :~: Zero nat
   leqZeroElim n nLE0 =
     case viewLeq n sZero nLE0 of
       LeqZero _ -> Refl
@@ -436,11 +436,11 @@
     coerceLeqL (plusComm n m) (l %:+ n) $
     coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl
 
-  succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero kproxy) -> Void
+  succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero nat) -> Void
   succLeqZeroAbsurd n leq =
     succNonCyclic n (leqZeroElim (sSucc n) leq)
 
-  succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero kproxy) :~: 'False
+  succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero nat) :~: 'False
   succLeqZeroAbsurd' n =
     case sSucc n %:<= sZero of
       STrue  -> absurd $ succLeqZeroAbsurd n Witness
@@ -588,7 +588,7 @@
   ltToLneq n m nLTm =
     coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm
 
-  lneqZero :: Sing (a :: nat) -> IsTrue (Zero kproxy :< Succ a)
+  lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat :< Succ a)
   lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n
 
   lneqSucc :: Sing (n :: nat) -> IsTrue (n :< Succ n)
@@ -606,6 +606,18 @@
                     -> m :~: Succ (Pred m)
   lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm
 
+  lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :< m) -> IsTrue (n :< m)
+  lneqSuccStepL n m snLNEQm =
+    coerce (sym $ lneqSuccLeq n m) $
+    leqSuccStepL (sSucc n) m $
+    coerce (lneqSuccLeq (sSucc n) m) snLNEQm
+
+  lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :< m) -> IsTrue (n :< Succ m)
+  lneqSuccStepR n m nLNEQm =
+    coerce (sym $ lneqSuccLeq n (sSucc m)) $
+    leqSuccStepR (sSucc n) m $
+    coerce (lneqSuccLeq n m) nLNEQm
+
   plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k
                      -> IsTrue (n :< m) -> IsTrue (l :< k)
                      -> IsTrue (n :+ l :< m :+ k)
@@ -617,16 +629,16 @@
         (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $
            coerce (lneqSuccLeq l k) lLNk)
 
-  maxZeroL :: Sing n -> Max (Zero kproxy) n :~: n
+  maxZeroL :: Sing n -> Max (Zero nat) n :~: n
   maxZeroL n = leqToMax sZero n (leqZero n)
 
-  maxZeroR  :: Sing n -> Max n (Zero kproxy) :~: n
+  maxZeroR  :: Sing n -> Max n (Zero nat) :~: n
   maxZeroR n = geqToMax n sZero (leqZero n)
 
-  minZeroL :: Sing n -> Min (Zero kproxy) n :~: Zero kproxy
+  minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat
   minZeroL n = leqToMin sZero n (leqZero n)
 
-  minZeroR  :: Sing n -> Min n (Zero kproxy) :~: Zero kproxy
+  minZeroR  :: Sing n -> Min n (Zero nat) :~: Zero nat
   minZeroR n = geqToMin n sZero (leqZero n)
 
   minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Succ n :- m :~: Succ (n :- m)
@@ -641,3 +653,7 @@
           === sSucc (k %:+ m %:- m)  `because` succCong (sym $ plusMinus k m)
           === sSucc (m %:+ k %:- m)  `because` succCong (minusCongL (plusComm k m) m)
           =~= sSucc (n %:- m)
+
+  lneqZeroAbsurd :: Sing n -> IsTrue (n :< Zero nat) -> Void
+  lneqZeroAbsurd n leq =
+    succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq)
diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs
--- a/Data/Type/Ordinal.hs
+++ b/Data/Type/Ordinal.hs
@@ -2,11 +2,12 @@
 {-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances       #-}
 {-# LANGUAGE GADTs, KindSignatures, LambdaCase, PatternSynonyms, PolyKinds #-}
 {-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving           #-}
-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators                  #-}
+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators      #-}
+{-# LANGUAGE ViewPatterns                                                  #-}
 -- | Set-theoretic ordinals for general peano arithmetic models
 module Data.Type.Ordinal
        ( -- * Data-types
-         Ordinal (..), HasOrdinal,
+         Ordinal (..), pattern OZ, pattern OS, HasOrdinal,
          -- * Conversion from cardinals to ordinals.
          sNatToOrd', sNatToOrd, ordToInt, ordToSing,
          ordToSing', CastedOrdinal(..),
@@ -19,6 +20,7 @@
          od
        ) where
 import           Control.Monad                (liftM)
+import           Data.Kind
 import           Data.List                    (genericDrop, genericTake)
 import           Data.Ord                     (comparing)
 import           Data.Singletons.Prelude
@@ -29,6 +31,7 @@
 import           Data.Type.Natural.Builtin    ()
 import           Data.Type.Natural.Class
 import           Data.Typeable                (Typeable)
+import           Data.Void                    (absurd)
 import           GHC.TypeLits                 (type (+))
 import qualified GHC.TypeLits                 as TL
 import           Language.Haskell.TH          hiding (Type)
@@ -36,11 +39,7 @@
 import           Proof.Equational
 import           Proof.Propositional
 import           Unsafe.Coerce
-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
-import Data.Kind
-#endif
 
-
 -- | Set-theoretic (finite) ordinals:
 --
 -- > n = {0, 1, ..., n-1}
@@ -49,65 +48,80 @@
 --
 --   Since 0.5.0.0
 data Ordinal (n :: nat) where
-  OZ  :: Sing n -> Ordinal (Succ n)
-  OS  :: Ordinal n -> Ordinal (Succ n)
-  OLt :: (n :< m) ~ 'True => Sing n -> Ordinal m
+  OLt :: (IsPeano nat, (n :< m) ~ 'True) => Sing (n :: nat) -> Ordinal m
 
+fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n :< Succ m) ~ 'True, SingI m)
+        => Sing (n :: nat) -> Ordinal m
+fromOLt  n =
+  case coerce (sym $ succLneqSucc n (sing :: Sing m)) Witness of
+    Witness -> OLt n
+
+-- | Pattern synonym representing the 0-th ordinal.
+pattern OZ :: forall nat (n :: nat). IsPeano nat
+           => (Zero nat :< n) ~ 'True => Ordinal n
+pattern OZ <- OLt Zero where
+  OZ = OLt sZero
+
+-- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal.
+pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t)
+            => (IsPeano nat)
+            => Ordinal t -> Ordinal (Succ t)
+pattern OS n <- OLt (Succ (fromOLt -> n)) where
+  OS o = succOrd o
+
 -- | Since 0.2.3.0
 deriving instance Typeable Ordinal
 
 -- |  Class synonym for Peano numerals with ordinals.
 --
 --  Since 0.5.0.0
-class (PeanoOrder kproxy, Monomorphicable (Sing :: nat -> *),
+class (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),
        Integral (MonomorphicRep (Sing :: nat -> *)),
-       SingKind kproxy, kproxy ~ 'KProxy,
-       Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal (kproxy :: KProxy nat)
-instance (PeanoOrder ('KProxy :: KProxy nat), Monomorphicable (Sing :: nat -> *),
+       Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat
+instance (PeanoOrder nat, Monomorphicable (Sing :: nat -> *),
        Integral (MonomorphicRep (Sing :: nat -> *)),
-       SingKind ('KProxy :: KProxy nat),
-       Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal ('KProxy :: KProxy nat)
+       Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat
 
-instance (HasOrdinal ('KProxy :: KProxy nat), SingI (n :: nat))
+instance (HasOrdinal nat, SingI (n :: nat))
       => Num (Ordinal n) where
   {-# SPECIALISE instance SingI n => Num (Ordinal (n :: PN.Nat))  #-}
   {-# SPECIALISE instance SingI n => Num (Ordinal (n :: TL.Nat))  #-}
   _ + _ = error "Finite ordinal is not closed under addition."
   _ - _ = error "Ordinal subtraction is not defined"
-  negate (OZ pxy) = OZ pxy
+  negate OZ = OZ
   negate _  = error "There are no negative oridnals!"
-  OZ pxy * _ = OZ pxy
-  _ * OZ pxy = OZ pxy
+  OZ * _ = OZ
+  _ * OZ = OZ
   _ * _  = error "Finite ordinal is not closed under multiplication"
   abs    = id
   signum = error "What does Ordinal sign mean?"
-  fromInteger = unsafeFromInt' (Proxy :: Proxy ('KProxy :: KProxy nat)) . fromInteger
+  fromInteger = unsafeFromInt' (Proxy :: Proxy nat) . fromInteger
 
 -- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n))
-instance (SingI n, HasOrdinal ('KProxy :: KProxy nat))
+instance (SingI n, HasOrdinal nat)
         => Show (Ordinal (n :: nat)) where
   {-# SPECIALISE instance SingI n => Show (Ordinal (n :: PN.Nat))  #-}
   {-# SPECIALISE instance SingI n => Show (Ordinal (n :: TL.Nat))  #-}
   showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (demote $ Monomorphic (sing :: Sing n)))
 
-instance (HasOrdinal ('KProxy :: KProxy nat))
+instance (HasOrdinal nat)
          => Eq (Ordinal (n :: nat)) where
   {-# SPECIALISE instance Eq (Ordinal (n :: PN.Nat))  #-}
   {-# SPECIALISE instance Eq (Ordinal (n :: TL.Nat))  #-}
   o == o' = ordToInt o == ordToInt o'
 
-instance (HasOrdinal ('KProxy :: KProxy nat)) => Ord (Ordinal (n :: nat)) where
+instance (HasOrdinal nat) => Ord (Ordinal (n :: nat)) where
   compare = comparing ordToInt
 
-instance (HasOrdinal ('KProxy :: KProxy nat), SingI n)
+instance (HasOrdinal nat, SingI n)
       => Enum (Ordinal (n :: nat)) where
   fromEnum = fromIntegral . ordToInt
-  toEnum   = unsafeFromInt' (Proxy :: Proxy ('KProxy :: KProxy nat)) . fromIntegral
+  toEnum   = unsafeFromInt' (Proxy :: Proxy nat) . fromIntegral
   enumFrom = enumFromOrd
   enumFromTo = enumFromToOrd
 
 enumFromToOrd :: forall (n :: nat).
-                 (HasOrdinal ('KProxy :: KProxy nat), SingI n)
+                 (HasOrdinal nat, SingI n)
               => Ordinal n -> Ordinal n -> [Ordinal n]
 enumFromToOrd ok ol =
   let k = ordToInt ok
@@ -115,27 +129,22 @@
   in genericTake (l - k + 1) $ enumFromOrd ok
 
 enumFromOrd :: forall (n :: nat).
-               (HasOrdinal ('KProxy :: KProxy nat), SingI n)
+               (HasOrdinal nat, SingI n)
             => Ordinal n -> [Ordinal n]
 enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n)
 
-enumOrdinal :: (SingKind ('KProxy :: KProxy nat), PeanoOrder ('KProxy :: KProxy nat), SingI n) => Sing (n :: nat) -> [Ordinal n]
+enumOrdinal :: (PeanoOrder nat, SingI n) => Sing (n :: nat) -> [Ordinal n]
 enumOrdinal (Succ n) = withSingI n $
   case lneqZero n of
     Witness ->
       OLt sZero : map succOrd (enumOrdinal n)
 enumOrdinal _ = []
 
-succOrd :: forall (n :: nat). (SingKind ('KProxy :: KProxy nat), PeanoOrder ('KProxy :: KProxy nat), SingI n) => Ordinal n -> Ordinal (Succ n)
+succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n)
 succOrd (OLt n) =
   case succLneqSucc n (sing :: Sing n) of
     Refl -> OLt (sSucc n)
-succOrd (OZ n) =
-  case (succLneqSucc sZero (sSucc n), lneqZero n) of
-    (Refl, Witness) -> OLt $ coerce (sym succOneCong) sOne
-succOrd (OS o) =
-  case (succLneqSucc sZero (sSucc (sing :: Sing n)), lneqZero (sing :: Sing n)) of
-    (Refl, Witness) -> OS (OS o)
+{-# INLINE succOrd #-}
 
 instance SingI n => Bounded (Ordinal ('PN.S n)) where
   minBound = OLt PN.SZ
@@ -155,7 +164,7 @@
   {-# INLINE maxBound #-}
 
 
-unsafeFromInt :: forall (n :: nat). (HasOrdinal ('KProxy :: KProxy nat), SingI (n :: nat))
+unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))
               => MonomorphicRep (Sing :: nat -> *) -> Ordinal n
 unsafeFromInt n =
     case promote (n :: MonomorphicRep (Sing :: nat -> *)) of
@@ -164,8 +173,8 @@
              STrue -> sNatToOrd' (sing :: Sing n) sn
              SFalse -> error "Bound over!"
 
-unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal ('KProxy :: KProxy nat), SingI n)
-              => proxy ('KProxy :: KProxy nat) -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n
+unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)
+              => proxy nat -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n
 unsafeFromInt' _ n =
     case promote (n :: MonomorphicRep (Sing :: nat -> *)) of
       Monomorphic sn ->
@@ -176,53 +185,33 @@
 -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.
 --
 --   Since 0.5.0.0
-sNatToOrd' :: (PeanoOrder ('KProxy :: KProxy nat), (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n
+sNatToOrd' :: (PeanoOrder nat, (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n
 sNatToOrd' _ m = OLt m
+{-# INLINE sNatToOrd' #-}
 
 -- | 'sNatToOrd'' with @n@ inferred.
-sNatToOrd :: (PeanoOrder ('KProxy :: KProxy nat), SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n
+sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n
 sNatToOrd = sNatToOrd' sing
 
 data CastedOrdinal n where
   CastedOrdinal :: (m :< n) ~ 'True => Sing m -> CastedOrdinal n
 
 -- | Convert @Ordinal n@ into @Sing m@ with the proof of @'S m :<= n@.
-ordToSing' :: forall (n :: nat). (PeanoOrder ('KProxy :: KProxy nat), SingI n) => Ordinal n -> CastedOrdinal n
-ordToSing' (OZ sk) =
-  case lneqZero sk of
-    (Witness) -> CastedOrdinal sZero
-ordToSing' (OS (on :: Ordinal k)) =
-  withSingI (sing :: Sing n) $
-  withPredSingI (Proxy :: Proxy k) (sing :: Sing n) $
-    case ordToSing' on of
-      CastedOrdinal m ->
-        case succLneqSucc m (sing :: Sing k) of
-          Refl -> CastedOrdinal (Succ m)
+ordToSing' :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> CastedOrdinal n
 ordToSing' (OLt s) = CastedOrdinal s
-
-withPredSingI :: forall proxy (n :: nat) r. PeanoOrder ('KProxy :: KProxy nat)
-              => proxy (n :: nat) -> Sing (Succ n) -> (SingI n => r) -> r
-withPredSingI pxy sn r = withSingI (sPred' pxy sn) r
-
+{-# INLINE ordToSing' #-}
 
 -- | Convert @Ordinal n@ into monomorphic @Sing@
 --
 -- Since 0.5.0.0
-ordToSing :: (PeanoOrder ('KProxy :: KProxy nat)) => Ordinal (n :: nat) -> SomeSing ('KProxy :: KProxy nat)
+ordToSing :: (PeanoOrder nat) => Ordinal (n :: nat) -> SomeSing nat
 ordToSing (OLt n) = SomeSing n
-ordToSing OZ{} = SomeSing sZero
-ordToSing (OS n) =
-  case ordToSing n of
-    SomeSing sn ->
-      case singInstance sn of
-        SingInstance -> SomeSing (Succ sn)
+{-# INLINE ordToSing #-}
 
 -- | Convert ordinal into @Int@.
-ordToInt :: (HasOrdinal ('KProxy :: KProxy nat), int ~ MonomorphicRep (Sing :: nat -> *))
+ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *))
          => Ordinal (n :: nat)
          -> int
-ordToInt OZ{} = 0
-ordToInt (OS n) = 1 + ordToInt n
 ordToInt (OLt n) = demote $ Monomorphic n
 {-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Integer #-}
 {-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-}
@@ -231,14 +220,6 @@
 inclusion' :: (n :< m) ~ 'True => Sing m -> Ordinal n -> Ordinal m
 inclusion' _ = unsafeCoerce
 {-# INLINE inclusion' #-}
-{-
--- The "proof" of the correctness of the above
-inclusion' :: (n :<= m) ~ 'True => Sing m -> Ordinal n -> Ordinal m
-inclusion' (SS SZ) OZ = OZ
-inclusion' (SS (SS _)) OZ = OZ
-inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m
-inclusion' _ _ = bugInGHC
--}
 
 -- | Inclusion function for ordinals with codomain inferred.
 inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m
@@ -247,43 +228,23 @@
 
 
 -- | Ordinal addition.
-(@+) :: forall n m. (PeanoOrder ('KProxy :: KProxy nat), SingI (n :: nat), SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
-OLt s @+ n =
-  case ordToSing' n of
-    CastedOrdinal n' ->
-      case plusStrictMonotone s (sing :: Sing n) n' (sing :: Sing m) Witness Witness of
-        Witness -> OLt $ s %:+ n'
-OZ {} @+ n =
-  let sn = sing :: Sing n
-      sm = sing :: Sing m
-  in case plusLeqR sn sm of
-      Witness -> inclusion n
-OS (n :: Ordinal k) @+ m =
-  withPredSingI n (sing :: Sing n) $
-  case sing :: Sing n of
-    Zero -> absurdOrd (OS n)
-    Succ sn ->
-      case singInstance sn of
-        SingInstance ->
-          let sm = sing :: Sing m
-              sn' = sing :: Sing n
-              sk  = sing :: Sing k
-              pf = start (sSucc (sk %:+ sm))
-                     === sSucc sk %:+ sm     `because` sym (plusSuccL sk sm)
-                     =~= sn' %:+ sm
-          in coerce pf $ OS $ n @+ m
-    _ -> error "inaccessible pattern"
+(@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m)
+     => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
+OLt k @+ OLt l =
+  let (n, m) = (n :: Sing n, m :: Sing m)
+  in case plusStrictMonotone k n l m Witness Witness of
+    Witness -> OLt $ k %:+ l
 
 -- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value.
 --
 -- Since 0.2.3.0
-absurdOrd :: PeanoOrder ('KProxy :: KProxy nat) => Ordinal (Zero ('KProxy :: KProxy nat)) -> a
-absurdOrd _cs = undefined -- case cs of {}
+absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a
+absurdOrd (OLt n) = absurd $ lneqZeroAbsurd n Witness
 
 -- | 'absurdOrd' for the value in 'Functor'.
 --
 --   Since 0.2.3.0
-vacuousOrd :: (PeanoOrder ('KProxy :: KProxy nat), Functor f) => f (Ordinal (Zero ('KProxy :: KProxy nat))) -> f a
+vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a
 vacuousOrd = fmap absurdOrd
 
 -- | 'absurdOrd' for the value in 'Monad'.
@@ -291,7 +252,7 @@
 --   become the superclass of 'Monad'.
 --
 --   Since 0.2.3.0
-vacuousOrdM :: (PeanoOrder ('KProxy :: KProxy nat), Monad m) => m (Ordinal (Zero ('KProxy :: KProxy nat))) -> m a
+vacuousOrdM :: (PeanoOrder nat, Monad m) => m (Ordinal (Zero nat)) -> m a
 vacuousOrdM = liftM absurdOrd
 
 -- | Quasiquoter for ordinals
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,13 +2,13 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.5.0.0
+version:             0.6.0.0
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
                      .
-                     This version 0.5.0.0 supports __GHC 7.10.* only__.
+                     Version 0.6+ supports __GHC 8+ only__.
                      .
-                     __Use >= 0.6.0.0 with GHC 8.0.0+__.
+                     __Use 0.5.* with ~ GHC 7.10.3__.
 homepage:            https://github.com/konn/type-natural
 license:             BSD3
 license-file:        LICENSE
@@ -45,7 +45,7 @@
                      , constraints               >= 0.3     && < 0.9
                      , ghc-typelits-natnormalise == 0.4.*
                      , ghc-typelits-presburger   >= 0.1.1   && < 1
-                     , singletons                == 2.1
+                     , singletons                == 2.2.*
 
   default-language:    Haskell2010
   default-extensions:  DataKinds