From 6cdbe556ddfb066a2fe205161b4ead793565c5f4 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Thu, 15 May 2025 23:20:43 +0200
Subject: Simplify lemRankApp

---
 src/Data/Array/Mixed/Lemmas.hs | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'src/Data/Array')

diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
index 7b3365b..7f41a06 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -56,20 +56,14 @@ lemRankApp :: forall sh1 sh2.
            -> Rank (sh1 ++ sh2) :~: Rank sh1 + Rank sh2
 lemRankApp ZKX _ = Refl
 lemRankApp (_ :!% (ssh1 :: StaticShX sh1T)) ssh2
-  = lem2 (Proxy @(Rank sh1T)) Proxy Proxy $
-      lem (Proxy @(Rank sh2)) (Proxy @(Rank sh1T)) (Proxy @(Rank (sh1T ++ sh2))) $
-        lemRankApp ssh1 ssh2
+  = lem (Proxy @(Rank sh1T)) Proxy Proxy $
+      sym (lemRankApp ssh1 ssh2)
   where
     lem :: proxy a -> proxy b -> proxy c
-        -> c :~: b + a
-        -> b + a :~: c
+        -> (a + b :~: c)
+        -> c + 1 :~: (a + 1 + b)
     lem _ _ _ Refl = Refl
 
-    lem2 :: proxy a -> proxy b -> proxy c
-         -> (a + b :~: c)
-         -> c + 1 :~: (a + 1 + b)
-    lem2 _ _ _ Refl = Refl
-
 lemRankAppComm :: StaticShX sh1 -> StaticShX sh2
                -> Rank (sh1 ++ sh2) :~: Rank (sh2 ++ sh1)
 lemRankAppComm _ _ = unsafeCoerceRefl  -- TODO improve this
-- 
cgit v1.2.3-70-g09d2