From aafe5f6b5fa772d0e2e9f9b4f91bc3e7cf696840 Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Wed, 19 Jun 2024 15:57:43 +0200
Subject: Add {m,r,s}dot1Inner

---
 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 633c9c2..ec7e7bd 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -108,6 +108,9 @@ lemTakeLenApp _ _ _ = unsafeCoerceRefl
 lemInitApp :: Proxy l -> Proxy x -> Init (l ++ '[x]) :~: l
 lemInitApp _ _ = unsafeCoerceRefl
 
+lemLastApp :: Proxy l -> Proxy x -> Last (l ++ '[x]) :~: x
+lemLastApp _ _ = unsafeCoerceRefl
+
 
 -- ** KnownNat
 
-- 
cgit v1.2.3-70-g09d2