induction hfull with
| empty =>
  simp [BTree.map]
  exact IsFull.empty
| node a l r hl hr hiff ihl ihr =>
  simp [BTree.map]
  apply IsFull.node
  { exact ihl }
  { exact ihr }
  { simp [BTree.map_eq_empty_iff]
    assumption }
α β : Type
f : α → β
t : BTree α
hfull : IsFull t
⊢ IsFull (map f t)
no goals