no goals
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : Sized l
hm : Sized m
hr : Sized r
⊢ Sized (Ordnode.node4L l x m y r)
cases m <;> [exact (hl.node' hm).node' hr; exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]