1 files changed, 5 insertions, 2 deletions
diff --git a/src/Lemmas.hs b/src/Lemmas.hs
index cb62155..31a43ed 100644
--- a/src/Lemmas.hs
+++ b/src/Lemmas.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 
 {-# LANGUAGE AllowAmbiguousTypes #-}
 module Lemmas (module Lemmas, (:~:)(Refl)) where
@@ -8,8 +9,10 @@ module Lemmas (module Lemmas, (:~:)(Refl)) where
 import Data.Type.Equality
 import Unsafe.Coerce (unsafeCoerce)
 
-import AST.Weaken
 
+type family Append a b where
+  Append '[] l = l
+  Append (x : xs) l = x : Append xs l
 
 lemAppendNil :: Append a '[] :~: a
 lemAppendNil = unsafeCoerce Refl