DEFINITION ex1_t()
TYPE =
       T
BODY =
THead
         Flat Appl
         TLRef O
         THead (Bind Abst) (TLRef (S (S O))) (TSort O)