(w{l2xy mono} (* coin *)
  (ite (* coin *)
    app
    app
  )
)
