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