From 3577c7dc9d3013d401c45a7628b0ff4b6fd0ec67 Mon Sep 17 00:00:00 2001
From: Raito Bezarius
Date: Fri, 12 Apr 2024 19:11:16 +0200
Subject: feat: upgrade and close all proofs except Preorder on U32

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>
---
 AvlVerification/Tree.lean | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'AvlVerification/Tree.lean')

diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean
index 3316e9e..fdd4b78 100644
--- a/AvlVerification/Tree.lean
+++ b/AvlVerification/Tree.lean
@@ -75,7 +75,4 @@ def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode.
 
 def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t)
 
-def AVLTree.setOf_left_incl (t: AVLTree T): t.left.set ⊂ t.set := sorry
-def AVLTree.setOf_right_incl (t: AVLTree T): t.right.set ⊂ t.set := sorry
-
 end Tree
-- 
cgit v1.2.3

