simp [mirror_Eq_empty_Iff, *]
case node.node.hiff
α : Type
a : α
l r : BTree α
ih_l : IsFull l → IsFull (mirror l)
ih_r : IsFull r → IsFull (mirror r)
hl : IsFull l
hr : IsFull r
hiff : l = BTree.empty ↔ r = BTree.empty
⊢ mirror r = BTree.empty ↔ mirror l = BTree.empty
no goals