1 files changed, 16 insertions, 1 deletions
diff --git a/src/Data.hs b/src/Data.hs
index 840cb88..4584a53 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE GADTs #-}
@@ -7,9 +8,10 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
-module Data where
+module Data (module Data, (:~:)(Refl)) where
 
 import Data.Type.Equality
+import Unsafe.Coerce (unsafeCoerce)
 
 import Lemmas (Append)
 
@@ -65,6 +67,16 @@ snatKnown :: SNat n -> Dict (KnownNat n)
 snatKnown SZ = Dict
 snatKnown (SS n) | Dict <- snatKnown n = Dict
 
+type family n + m where
+  Z + m = m
+  S n + m = S (n + m)
+
+lemPlusSuccRight :: n + S m :~: S (n + m)
+lemPlusSuccRight = unsafeCoerceRefl
+
+lemPlusZero :: n + Z :~: n
+lemPlusZero = unsafeCoerceRefl
+
 data Vec n t where
   VNil :: Vec Z t
   (:<) :: t -> Vec n t -> Vec (S n) t
@@ -83,3 +95,6 @@ vecGenerate = \n f -> go n f SZ
     go :: SNat n -> (forall i. SNat i -> t) -> SNat i' -> Vec n t
     go SZ _ _ = VNil
     go (SS n) f i = f i :< go n f (SS i)
+
+unsafeCoerceRefl :: a :~: b
+unsafeCoerceRefl = unsafeCoerce Refl