(match (* t *)
  (w{mono} (* proof leaf 1 *)
    leaf
  )
  (ite (* a ⩵ c *)
    (w{mono} (* proof leaf 3 *)
      node
    )
    (ite (* a ⪱ c *)
      (match (* cl *)
        (w{mono} (* first after match *)
          (let:tree:cf
            leaf
            (w{mono} (* size because binds a leaf *)
              (let:tree:cf
                leaf
                (w{mono} (* size because binds a leaf *)
                  (let:tree:cf
                    node
                    (w{mono} (* proof leaf 2 *)
                      node
                    )
                  )
                )
              )
            )
          )
        )
        (ite (* a ⩵ b *)
          (w{mono} (* first after match *)
            (let:tree:cf
              node
              (w{mono} (* proof leaf 2 *)
                node
              )
            )
          )
          (ite (* a ⪱ b *)
            (match (* bl *)
              (w{mono} (* first after match *)
                (let:tree:cf
                  leaf
                  (w{mono} (* size because binds a leaf *)
                    (let:tree:cf
                      leaf
                      (w{mono} (* size because binds a leaf *)
                        (let:tree:cf
                          node
                          (let:tree:cf
                            node
                            (w{mono} (* proof leaf 2 *)
                              node
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
              (w{l2xy mono} (* binds a call/tick *)
                (let:tree:cf
                  (tick
                    (shift
                      app
                    )
                  )
                  (match (* ~ 1 2 insert a bl *)
                    (w{mono} (* proof leaf 1 *)
                      (w:var
                        (w:var
                          leaf
                        )
                      )
                    )
                    (w{l2xy} (* first after call, before ite:coin *) (* coin *)
                      (ite (* coin *)
                        (w{mono} (* tick outside let *)
                          (tick
                            (let:tree:cf
                              node
                              (let:tree:cf
                                node
                                (w{mono} (* proof leaf 2 *)
                                  node
                                )
                              )
                            )
                          )
                        )
                        (w{mono} (* first after match *)
                          (let:tree:cf
                            node
                            (let:tree:cf
                              node
                              (w{mono} (* proof leaf 2 *)
                                node
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
            (match (* br *)
              (w{mono} (* first after match *)
                (let:tree:cf
                  leaf
                  (w{mono} (* size because binds a leaf *)
                    (let:tree:cf
                      leaf
                      (w{mono} (* size because binds a leaf *)
                        (let:tree:cf
                          node
                          (let:tree:cf
                            node
                            (w{mono} (* proof leaf 2 *)
                              node
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
              (w{l2xy mono} (* binds a call/tick *)
                (let:tree:cf
                  (tick
                    (shift
                      app
                    )
                  )
                  (match (* ~ 1 2 insert a br *)
                    (w{mono} (* proof leaf 1 *)
                      (w:var
                        (w:var
                          leaf
                        )
                      )
                    )
                    (w{l2xy} (* first after call, before ite:coin *) (* coin *)
                      (ite (* coin *)
                        (w{mono} (* tick outside let *)
                          (tick
                            (let:tree:cf
                              node
                              (let:tree:cf
                                node
                                (w{mono} (* proof leaf 2 *)
                                  node
                                )
                              )
                            )
                          )
                        )
                        (w{mono} (* first after match *)
                          (let:tree:cf
                            node
                            (let:tree:cf
                              node
                              (w{mono} (* proof leaf 2 *)
                                node
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
      (match (* cr *)
        (w{mono} (* first after match *)
          (let:tree:cf
            leaf
            (w{mono} (* size because binds a leaf *)
              (let:tree:cf
                leaf
                (w{mono} (* size because binds a leaf *)
                  (let:tree:cf
                    node
                    (w{mono} (* proof leaf 2 *)
                      node
                    )
                  )
                )
              )
            )
          )
        )
        (ite (* a ⩵ b *)
          (w{mono} (* first after match *)
            (let:tree:cf
              node
              (w{mono} (* proof leaf 2 *)
                node
              )
            )
          )
          (ite (* a ⪱ b *)
            (match (* bl *)
              (w{mono} (* first after match *)
                (let:tree:cf
                  leaf
                  (w{mono} (* size because binds a leaf *)
                    (let:tree:cf
                      leaf
                      (w{mono} (* size because binds a leaf *)
                        (let:tree:cf
                          node
                          (let:tree:cf
                            node
                            (w{mono} (* proof leaf 2 *)
                              node
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
              (w{l2xy mono} (* binds a call/tick *)
                (let:tree:cf
                  (tick
                    (shift
                      app
                    )
                  )
                  (match (* ~ 1 2 insert a bl *)
                    (w{mono} (* proof leaf 1 *)
                      (w:var
                        (w:var
                          leaf
                        )
                      )
                    )
                    (w{l2xy} (* first after call, before ite:coin *) (* coin *)
                      (ite (* coin *)
                        (w{mono} (* tick outside let *)
                          (tick
                            (let:tree:cf
                              node
                              (let:tree:cf
                                node
                                (w{mono} (* proof leaf 2 *)
                                  node
                                )
                              )
                            )
                          )
                        )
                        (w{mono} (* first after match *)
                          (let:tree:cf
                            node
                            (let:tree:cf
                              node
                              (w{mono} (* proof leaf 2 *)
                                node
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
            (match (* br *)
              ? (*w{mono} (* first after match *)
                (let:tree:cf
                  node
                  (let:tree:cf
                    leaf
                    (w{mono} (* size because binds a leaf *)
                      (let:tree:cf
                        leaf
                        (w{mono} (* size because binds a leaf *)
                          (let:tree:cf
                            node
                            (w{mono} (* proof leaf 2 *)
                              ? (* node *) (* Problem. *)
                            )
                          )
                        )
                      )
                    )
                  )
                )
              *)
              (w{l2xy mono} (* binds a call/tick *)
                (let:tree:cf
                  (tick
                    (shift
                      app
                    )
                  )
                  (match (* ~ 1 2 insert a br *)
                    (w{mono} (* proof leaf 1 *)
                      (w:var
                        (w:var
                          leaf
                        )
                      )
                    )
                    (w{l2xy} (* first after call, before ite:coin *) (* coin *)
                      (ite (* coin *)
                        (w{mono} (* tick outside let *)
                          (tick
                            (let:tree:cf
                              node
                              (let:tree:cf
                                node
                                (w{mono} (* proof leaf 2 *)
                                  node
                                )
                              )
                            )
                          )
                        )
                        (w{mono} (* first after match *)
                          (let:tree:cf
                            node
                            (let:tree:cf
                              node
                              (w{mono} (* proof leaf 2 *)
                                node
                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
              )
            )
          )
        )
      )
    )
  )
)
