have fmmt : IsFull (mirror (mirror t)) :=
  IsFull_mirror _ fmt
α : Type
t : BTree α
fmt : IsFull (mirror t)
⊢ IsFull t
α : Type
t : BTree α
fmt : IsFull (mirror t)
fmmt : IsFull (mirror (mirror t))
⊢ IsFull t