1 files changed, 22 insertions, 2 deletions
diff --git a/src/Data/INat.hs b/src/Data/INat.hs
index 7a495ca..2d65c53 100644
--- a/src/Data/INat.hs
+++ b/src/Data/INat.hs
@@ -13,9 +13,10 @@
 module Data.INat where
 
 import Data.Proxy
+import Data.Type.Equality ((:~:) (Refl))
 import Numeric.Natural
 import GHC.TypeLits
-
+import Unsafe.Coerce (unsafeCoerce)
 
 -- | Evidence for the constraint @c a@.
 data Dict c a where
@@ -73,10 +74,29 @@ type family FromINat n where
   FromINat (S n) = 1 + FromINat n
 
 -- | Convert a "GHC.TypeLits" 'G.Nat' to a 'INat'.
-type family ToINat n where
+type family ToINat (n :: Nat) where
   ToINat 0 = Z
   ToINat n = S (ToINat (n - 1))
 
+lemInjectiveFromINat :: n :~: ToINat (FromINat n)
+lemInjectiveFromINat = unsafeCoerce Refl
+
+lemSuccFromINat :: Proxy n -> 1 + FromINat n :~: FromINat (S n)
+lemSuccFromINat _ = unsafeCoerce Refl
+
+lemAddFromINat :: Proxy m -> Proxy n
+               -> FromINat m + FromINat n :~: FromINat (m +! n)
+lemAddFromINat _ = unsafeCoerce Refl
+
+lemInjectiveToINat :: n :~: FromINat (ToINat n)
+lemInjectiveToINat = unsafeCoerce Refl
+
+lemSuccToINat :: Proxy n -> ToINat (1 + n) :~: S (ToINat n)
+lemSuccToINat _ = unsafeCoerce Refl
+
+lemAddToINat :: Proxy m -> Proxy n -> ToINat (m + n) :~: ToINat m +! ToINat n
+lemAddToINat _ _ = unsafeCoerce Refl
+
 -- | If an inductive 'INat' is known, then the corresponding "GHC.TypeLits"
 -- 'G.Nat' is also known.
 knownNatFromINat :: KnownINat n => Proxy n -> Dict KnownNat (FromINat n)