cons-tail := λ(: tt Type). (: (
   (let r TAny)
   (match tt (
      ()
      ( (TGround( 'Cons_s (LCons( tl (LCons( hd LEOF )) )) )) (set r tl) )
      ( _ () )
   ))
   r
) Type);