(match (* t *)
  (w leaf)
  (match (* cl, zig *)
    (w leaf)
    (match (* bl, zig zig *)
      (w leaf)
      (w{l2xy} (let:tree:cf
        (tick app) (* _ a bl *)
        (match
          (w leaf)
          (ite (* coin *)
            (tick (let:tree:cf node (let:tree:cf node (w{mono} node))))
            (let:tree:cf (w node) (let:tree:cf (w{mono} node) (w node)))
          )
        )
      ))
    )
  )
)