abstract Lex = Cat ** {
  fun
    zero_PN : PN ;
    successor_N2 : N2 ;  
    even_A : A ;
}