From ce4ea63db5e11b150058894f98b4a36a3003c95a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 23 Apr 2024 17:45:31 -0500
Subject: Add merge and unmerge properties

---
 Util.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Util.agda')

diff --git a/Util.agda b/Util.agda
index 0c79b17..d7053c5 100644
--- a/Util.agda
+++ b/Util.agda
@@ -27,6 +27,6 @@ compare Fin.zero Fin.zero = equal refl
 compare Fin.zero j@(Fin.suc _) = less (z<s , toℕ< j)
 compare i@(Fin.suc _) Fin.zero = greater (z<s , toℕ< i)
 compare (Fin.suc i) (Fin.suc j) with compare i j
-... | less (i<j , j<n) = less (_≤_.s≤s i<j , _≤_.s≤s j<n)
+... | less (i<j , j<n) = less (s≤s i<j , s≤s j<n)
 ... | equal i≡j = equal (cong Fin.suc i≡j)
-... | greater (j<i , i<n) = greater (_≤_.s≤s j<i , _≤_.s≤s i<n)
+... | greater (j<i , i<n) = greater (s≤s j<i , s≤s i<n)
-- 
cgit v1.2.3