{-# 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