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