menu

ZF_Base
upair
pair
equalities
Fixedpt
Bool
Sum
func
QPair
Perm
Trancl
WF
Ordinal
OrdQuant
Nat
Inductive
Epsilon
Order
OrderArith
OrderType
Finite
Cardinal
Univ
QUniv
Datatype
Arith
ArithSimp
List
EquivClass
Int
Bin
IntDiv
CardinalArith
ZF
AC
Zorn
Cardinal_AC
InfDatatype
ZFC

ZF.ArithSimp

HTML Presentation