{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
module Lemmas (module Lemmas, (:~:)(Refl)) where

import Data.Type.Equality
import Unsafe.Coerce (unsafeCoerce)

import AST.Weaken


lemAppendNil :: Append a '[] :~: a
lemAppendNil = unsafeCoerce Refl

lemAppendAssoc :: Append a (Append b c) :~: Append (Append a b) c
lemAppendAssoc = unsafeCoerce Refl