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