simp [BTree.map]
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (map f (node a l r))
case node
α β : Type
f : α → β
t : BTree α
a : α
l r : BTree α
hl : IsFull l
hr : IsFull r
hiff : l = empty ↔ r = empty
ihl : IsFull (map f l)
ihr : IsFull (map f r)
⊢ IsFull (node (f a) (map f l) (map f r))