compose = f g x : f (g x)

succ = y (self :
  triage
    1
    t
    (triage
      (t (t t))
      (_ tail : t t (self tail))
      t))

size = (x :
  (y (self x :
    compose succ
      (triage
        (x : x)
        self
        (x y : compose (self x) (self y))
        x)) x 0))

size size