no goals
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : Sized m
⊢ size (node4L l x m y r) = size l + size m + size r + 2
cases m <;> simp [node4L, node3L, node'] <;> [skip; simp [size, hm.1]] <;> abel