exact ihl
case node.hl
α β : 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 l)
no goals