feat: factor everything in `OrdSpecRel`

Now, we speak only about equivalence.

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>

2 files changed, 2 insertions, 6 deletions

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)
diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean
index 0694df3..ac2d056 100644
--- a/AvlVerification/Specifications.lean
+++ b/AvlVerification/Specifications.lean
@@ -53,14 +53,10 @@ class OrdSpecInfaillible where
 class OrdSpecDuality extends OrdSpecInfaillible H where
   duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less
 
--- TODO: OrdSpecEq := OrdSpecRel (R := Eq).
-class OrdSpecEq extends OrdSpecInfaillible H where
-  equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b
-
 class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where
   equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b
 
-class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecEq H
+class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecRel H Eq
 
 instance: Coe (avl_verification.Ordering) (_root_.Ordering) where
   coe a := a.toLeanOrdering