intro ht
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
⊢ IsFull (BTree.node a l r) → IsFull (mirror (BTree.node a l r))
case node
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
ht : IsFull (BTree.node a l r)
⊢ IsFull (mirror (BTree.node a l r))