(w{l2xy mono} (* binds a call/tick *)
  (let:tree:cf
    (tick
      app
    )
    (match (* ~ 1 2 insert_dummy bl *)
      (w{mono} (* proof leaf 1 *)
        (w:var
          (w:var
            leaf
          )
        )
      )
      (w{mono} app)
    )
  )
)
