1 files changed, 0 insertions, 21 deletions
diff --git a/src/Lemmas.hs b/src/Lemmas.hs
deleted file mode 100644
index 31a43ed..0000000
--- a/src/Lemmas.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-
-{-# LANGUAGE AllowAmbiguousTypes #-}
-module Lemmas (module Lemmas, (:~:)(Refl)) where
-
-import Data.Type.Equality
-import Unsafe.Coerce (unsafeCoerce)
-
-
-type family Append a b where
-  Append '[] l = l
-  Append (x : xs) l = x : Append xs l
-
-lemAppendNil :: Append a '[] :~: a
-lemAppendNil = unsafeCoerce Refl
-
-lemAppendAssoc :: Append a (Append b c) :~: Append (Append a b) c
-lemAppendAssoc = unsafeCoerce Refl