Entry	Value
Package Name	unit-thm
Count	4
Theorems	one_Axiom : !e. ?!fn. fn one = e one_INDUCT : !p. p one ==> (!x. p x) one_RECURSION : !e. ?fn. fn one = e one_axiom : !f g. f = g

Back to main package page