test fix

agda · Dec 9, 2024 · 1aece6a · 1aece6a
1 parent 31b7c6a
commit 1aece6a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/LawfulOrd.agda b/test/LawfulOrd.agda
@@ -13,7 +13,7 @@ nLtEq2Gt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
 nLtEq2Gt x y ⦃ h1 ⦄ ⦃ h2 ⦄ =
   begin
     (x > y)
-  ≡⟨ sym (not-involution (x <= y) (x > y) (lte2ngt x y)) ⟩
+  ≡⟨ sym (not-involution (lte2ngt x y)) ⟩
     not (x <= y)
   ≡⟨ cong not (lte2LtEq x y) ⟩
     not ((x < y) || (x == y))