Theory: one

Parents

• bool

Types

• one(Arity = 0)

Constants

• one  :one

Definitions

one_DEF

|- one = @x. T

one_TY_DEF

|- ?rep. TYPE_DEFINITION (\b. b) rep

Theorems

one

|- !v. v = one

one_Axiom

|- !e. ?!fn. fn one = e