is-sized := λ(: tt Type). (: (
   (let r 0_u64)
   (match tt (
      ()
      ( TAny (set r 1_u64) )
      ( (TGround( 'Cons_s _ )) (set r 1_u64) )
      ( (TGround( 'Arrow_s _ )) (set r 1_u64) )
      ( (TGround( 'Sized_s _ )) (set r 1_u64) )
      ( (TAnd( lt rt )) (
         (set r (max(
            (is-sized lt)
            (is-sized rt)
         )))
      ))
      ( _ () )
   ))
   r
) U64);