Type constraint added to ensure that "length" refers to lists. Maybe should
not be needed, but the translation length->size happens irrespective of types
intro Introduction to Isabelle
ref The Isabelle Reference Manual
system The Isabelle System Manual
logics Isabelle's Object-Logics
ind-defs (Co)Inductive Definitions in ZF
axclass Tutorial on Axiomatic Type Classes