cons-arity := λ(: tt Type). (: (
   (let a 1_u64)
   (match tt (
      ()
      ( (TGround( 'Cons_s (LCons( rtt (LCons( ltt LEOF )) )) )) (
         (set a (+( (cons-arity ltt) 1_u64 )))
      ))
      ( _ () )
   ))
   a
) U64);