(let:tree:cf
  (tick app) (* splay a t *)
  (match
    (w leaf)
    (ite (* a == a1 *)
      (match (* l *)
        (w var)
        (w{mono l2xy} (let:tree:cf
          (tick app)
          (match (* splay_max l *)
            leaf
            (w node)
          )
        ))
      )
      (w node)
    )
  )
)