data List a << p:a (fld:a)>> = Nil | Cons x:a^True y:List a^p(x) << p(fld) >> --