moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
List = FOL +
types list 1
arities list :: (term)term
consts Nil :: "'a list"
Cons :: "['a, 'a list] => 'a list"
end