induction t with
| empty =>
  rfl
| node a l r ih_l ih_r =>
  rw [Multiset.elems]
  rw [mirror]
  rw [←ih_l]
  rw [←ih_r]
  rw [Multiset.elems]
  rw [Multiset.union_assoc,
      Multiset.union_comm (elems (mirror r)),
      ←Multiset.union_assoc]
t : BTree ℕ
⊢ elems (mirror t) = elems t
no goals