DEFINITION TApp()
TYPE =
       TListTTList
BODY =
FIXTApp{
         TApp:TListTTList
         :=λts:TList
           .λv:T
             .<λt:TList.TList>
               CASE ts OF
                 TNilTCons v TNil
               | TCons t ts0TCons t (TApp ts0 v)
         }