tricu/demos/size.tri

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