From fb9a1e93c2163b170979523f9a0cae90b472a16c Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Wed, 17 Apr 2024 16:50:16 +0200
Subject: feat: factor everything in `OrdSpecRel`

Now, we speak only about equivalence.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Insert.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'AvlVerification/Insert.lean')

diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean
index 16e740f..f5b7958 100644
--- a/AvlVerification/Insert.lean
+++ b/AvlVerification/Insert.lean
@@ -134,7 +134,7 @@ lemma AVLTreeSet.insert_loop_spec_global
     {
       simp; split_conjs
       . tauto
-      . simp [Ospec.equality _ _ Hordering]
+      . simp [Ospec.equivalence _ _ Hordering]
     }
     {
       have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst)
-- 
cgit v1.2.3

