(match (* t *)
  (w{mono} (let:tree:cf leaf (let:tree:cf leaf node)))
  (w{mono l2xy} (let:tree:cf
    (tick app) (* splay_eq a t *)
    (match
      (w leaf)
      (ite (* a == a' *)
        (w node)
        (ite (* a < a' *)
          (w{mono} (let:tree:cf leaf (let:tree:cf node node)))
          (w{mono} (let:tree:cf leaf (let:tree:cf node node)))
        )
      )
    )
  ))
)