type
sort
object
binder
attribution
application
constant
semantic-attribution
error
global
local
informal
simple
implicit
pattern
inductive
satisfiable
counter-satisfiable
no-consequence
theorem
conter-theorem
contradictory-axioms
tautologous-conclusion
tautology
equivalent
conunter-equivalent
unsatisfiable-conclusion
unsatisfiable
just-by, points to the theorem justifying well-definedness
entailed-by, entails, point to other (equivalent definitions
entailed-by-thm, entails-thm point to the theorems justifying
the entailment relation)
for
against
official
experimental
private
obsolete