diff options
Diffstat (limited to '')
| -rw-r--r-- | AvlVerification/Insert.lean | 2 |
1 files changed, 1 insertions, 1 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) |