DEFINITION THeads()
TYPE =
       K→TList→T→T
BODY =
FIXTHeads{
         THeads:K→TList→T→T
         :=λk:K
           .λus:TList
             .λt:T
               .<λt1:TList.T> CASE us OF TNil⇒t | TCons u ul⇒THead k u (THeads k ul t)
         }