α : Type u_1
t : Ordnode α
h : Sized (Ordnode.dual t)
⊢ Sized (Ordnode.dual (Ordnode.dual t))
α : Type u_1
t : Ordnode α
h : Sized (Ordnode.dual t)
⊢ Sized t
rw [← dual_dual t]
no goals
α : Type u_1
t : Ordnode α
h : Sized (Ordnode.dual t)
⊢ Sized (Ordnode.dual (Ordnode.dual t))
exact h.dual