1 files changed, 6 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs
index c3381d5..a3f4c3c 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -8,6 +8,8 @@
 {-# LANGUAGE TypeOperators #-}
 module Data where
 
+import Lemmas (Append)
+
 
 data SList f l where
   SNil :: SList f '[]
@@ -19,6 +21,10 @@ slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list
 slistMap _ SNil = SNil
 slistMap f (SCons x list) = SCons (f x) (slistMap f list)
 
+sappend :: SList f l1 -> SList f l2 -> SList f (Append l1 l2)
+sappend SNil l = l
+sappend (SCons x xs) l = SCons x (sappend xs l)
+
 data Nat = Z | S Nat
   deriving (Show, Eq, Ord)