From 0d6f77762d1697ea41b190e550f94e459079e3d1 Mon Sep 17 00:00:00 2001
From: Mikolaj Konarski <mikolaj.konarski@funktory.com>
Date: Sat, 17 May 2025 00:04:53 +0200
Subject: Eliminate the dependency cycle of Lemmas modules

---
 src/Data/Array/Mixed/Lemmas.hs | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'src/Data/Array/Mixed')

diff --git a/src/Data/Array/Mixed/Lemmas.hs b/src/Data/Array/Mixed/Lemmas.hs
index ded6af5..e6d970c 100644
--- a/src/Data/Array/Mixed/Lemmas.hs
+++ b/src/Data/Array/Mixed/Lemmas.hs
@@ -17,15 +17,6 @@ import Data.Array.Nested.Permutation
 import Data.Array.Nested.Types
 
 
--- * Reasoning helpers
-
-subst1 :: forall f a b. a :~: b -> f a :~: f b
-subst1 Refl = Refl
-
-subst2 :: forall f c a b. a :~: b -> f a c :~: f b c
-subst2 Refl = Refl
-
-
 -- * Lemmas
 
 -- ** Nat
-- 
cgit v1.2.3-70-g09d2