From 4a0b2ef27a6e31250c56faef0efc0abf611a0cda Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 18 Jun 2024 21:04:23 +0200
Subject: Init on ListX

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

(limited to 'src/Data/Array/Mixed/Lemmas.hs')

diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
index ff2e45c..633c9c2 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -105,6 +105,9 @@ lemTakeLenApp :: Rank l1 <= Rank l2
               -> TakeLen l1 l2 :~: TakeLen l1 (l2 ++ rest)
 lemTakeLenApp _ _ _ = unsafeCoerceRefl
 
+lemInitApp :: Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l
+lemInitApp _ _ = unsafeCoerceRefl
+
 
 -- ** KnownNat
 
-- 
cgit v1.2.3-70-g09d2