Entry	Value
Package Name	function-def
Count	8
Theorems	C_DEF : C = (\f x y. f y x) I_DEF : I = (\x. x) K_DEF : K = (\x y. x) ONE_ONE : !f. ONE_ONE f <=> (!x1 x2. f x1 = f x2 ==> x1 = x2) ONTO : !f. ONTO f <=> (!y. ?x. y = f x) S_DEF : S = (\f g x. f x (g x)) W_DEF : W = (\f x. f x x) o_PRIM_DEF : (o) = (\f g x. f (g x))

Back to main package page