exact ih_r
case node.hl
α : Type
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
ih_l : IsFull (mirror l)
ih_r : IsFull (mirror r)
⊢ IsFull (mirror r)
no goals