The translation of lists, although correct, is really ugly.

---------------------------------------------------------
    Nil : b_0
    Conc : b_0 * b_0 -> b_0
    Conc : b_0 * a_0 -> a_0
    Conc : a_0 * b_0 -> a_0
    Conc : a_0 * a_0 -> a_0
    Cons : Id * b_0 -> a_0
---------------------------------------------------------

This must be improved. ASAP. Maybe it is possible to recognize such a structure in rtg2sig and use the List(...) in this case. It is a pity that the signature isn't that precise anymore then, but well ... Het oog wil ook wat!