Avoiding potentially common pitfalls
This topic is initially little more than a stub. It is a place to
list things to keep in mind in order to avoid potentially common mistakes.
It may be tempting to ignore the tag-tree (ttree) returned by a
function. But tag-trees may contain assumption records, stored under the
tag 'assumption, that record forced assumptions to be proved
later (in forcing rounds or, in the case of case-split or immediate-force-modep, more immediately). So it can be unsound to ignore
tag-trees unless they are sure not to contain assumptions (see