induction t with
| empty                =>
  { intro ht
    exact ht }
| node a l r ih_l ih_r =>
  { intro ht
    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, *] } } }
α : Type
t : BTree α
⊢ IsFull t → IsFull (mirror t)
no goals