cases ht with
| node _ _ _ hl hr hiff =>
  { rw [mirror]
    apply IsFull.node
    { exact ih_r hr }
    { apply ih_l hl }
    { simp [mirror_Eq_empty_Iff, *] } }
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))
no goals