induction ht with
| empty                           => exact IsFull.empty
| node a l r hl hr hiff ih_l ih_r =>
  { rw [mirror]
    apply IsFull.node
    { exact ih_r }
    { exact ih_l }
    { simp [mirror_Eq_empty_Iff, *] } }
α : Type
t : BTree α
ht : IsFull t
⊢ IsFull (mirror t)
no goals