test fix

odderwiser · odderwiser · commit 1aece6a70777 · 2024-12-09T16:11:10.000+01:00
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))
