% Mix lists and counting together. typedec0 "nil" bottom null\ typedec2 "cons" (x\l\ stroke par l) cons\ typedec0 "z" bottom z\ typedec1 "s" (n\ stroke par n) s\ typedec2 "length" (l\n\ l o-o n) length\ clauses ( (length null z) && (qi "X" X\ qi "L" L\ qi "N" N\ length (cons X L) (s N) <== length L N) ).