(match (* h *)
  (w{l2xy size} leaf)
  (w{l2xy size} (match
    (w{l2xy size} (let:tree:cf (w{l2xy size} leaf) (w{size l2xy} node)))
    (ite
      (w{l2xy size} (let:tree:cf (w{size l2xy} node) (w{size l2xy} node)))
      (w{l2xy size} (let:tree:cf (w{size l2xy} node) (w{size l2xy} node)))
    )
  ))
)