Derivetermbounds can be improved

[Bart Bogaerts]

Consider the following example:

vocabulary StolCoinsVoc {

type Coins isa nat Stolen(Coins):nat

}

theory StolenCoins : StolCoinsVoc {

sum{ c[Coins] : true : c * Stolen(c) } = 100.

}

Termbounds for c*Stolen(c) and even for Stolen(c) can be derived.