Coding out subsorting into unary predicates. New concept for proving Ontologies.

generatedness via non-injective datatype constructors (i.e. proper data constructors) is simply ignored

total functions my become partial because i.e. division is total for a second non-zero argument but partial otherwise.

partial functions remain partial unless they fall to together with an overloaded total function