{ exact IsFull.empty }
case hr
α : Type
a : α
⊢ IsFull BTree.empty

case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
case hiff
α : Type
a : α
⊢ BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty