Other References

Find the Miscellaneous section of the display for #$TeethCleaning. The Miscellaneous section is not automatically displayed, but you will see a clickable link at the bottom of the frame on the left. Click on this link and a page with the Miscellaneous assertions will be displayed.

The Miscellaneous section of a constant page contains assertions that refer somewhere to the displayed term, but do not have the term as one of their top-level arguments, and don't have it indexed in some other way.

If a collection, such as #$TeethCleaning, is mentioned in an implication axiom as an argument to #$isa, the axiom shows up in the Antecedent orConsequent section of the page.

If a constant is not a collection, or is used in one of the literals of an implication statement as an argument to a predicate other than #$isa, the axiom will appear in the Miscellaneous section.

Sometimes ground atomic formulae (also called GAFs) appear in the Miscellaneous section. This happens if one of their arguments is a list or some other complex structure containing the displayed term. GAFs are atomic formulae, i.e., a predicate followed by its arguments, in which all of the arguments are bound -- none of them are variables.