From 2a53042c1ce8b593a6178696c03ac77c6b76b395 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Thu, 25 Jan 2024 21:46:29 +0100
Subject: Finish rewrite

---
 src/Lemmas.hs | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Lemmas.hs')

diff --git a/src/Lemmas.hs b/src/Lemmas.hs
index 7dbf680..cb62155 100644
--- a/src/Lemmas.hs
+++ b/src/Lemmas.hs
@@ -11,5 +11,8 @@ 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
-- 
cgit v1.2.3-70-g09d2